{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# 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 Data.Coerce
import Data.Function
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.GHC.Compat hiding (Node)
import Development.IDE.GHC.Orphans ()
import GHC.Generics
import GHC.SourceGen (var)
import InstEnv (InstEnvs(..))
import OccName
import Refinery.Tactic
import System.IO.Unsafe (unsafePerformIO)
import Type (TCvSubst, Var, eqType, nonDetCmpType, emptyTCvSubst)
import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
import Wingman.Debug
import Wingman.FeatureSet
data TacticCommand
= Auto
| Intros
| Destruct
| Homomorphism
| DestructLambdaCase
| HomomorphismLambdaCase
| DestructAll
| UseDataCon
| Refine
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)
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
Destruct a
var = a
"Case split on " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
var
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"
data Config = Config
{ Config -> FeatureSet
cfg_feature_set :: FeatureSet
, Config -> Int
cfg_max_use_ctor_actions :: Int
, Config -> Int
cfg_timeout_seconds :: Int
}
newtype CType = CType { CType -> Type
unCType :: Type }
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 OccName where
show :: OccName -> String
show = OccName -> String
forall a. Outputable a => a -> String
unsafeRender
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 (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
data TacticState = TacticState
{ TacticState -> Set Var
ts_skolems :: !(Set TyVar)
, 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>"
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
'🚒'
{-# 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
}
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
data Provenance
=
TopLevelArgPrv
OccName
Int
Int
| PatternMatchPrv PatVal
| ClassMethodPrv
(Uniquely Class)
| UserPrv
| RecursivePrv
| 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)
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)
data PatVal = PatVal
{ PatVal -> Maybe OccName
pv_scrutinee :: Maybe OccName
, PatVal -> Set OccName
pv_ancestry :: Set OccName
, PatVal -> Uniquely ConLike
pv_datacon :: Uniquely ConLike
, PatVal -> Int
pv_position :: Int
} 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)
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
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
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)
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)
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)
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
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
}
deriving stock (Judgement' a -> Judgement' a -> Bool
(Judgement' a -> Judgement' a -> Bool)
-> (Judgement' a -> Judgement' a -> Bool) -> Eq (Judgement' a)
forall a. Eq a => Judgement' a -> Judgement' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Judgement' a -> Judgement' a -> Bool
$c/= :: forall a. Eq a => Judgement' a -> Judgement' a -> Bool
== :: Judgement' a -> Judgement' a -> Bool
$c== :: forall a. Eq a => Judgement' a -> Judgement' a -> Bool
Eq, (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 a = { :: Reader Context 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)
instance MonadExtract (Synthesized (LHsExpr GhcPs)) ExtractM where
hole :: ExtractM (Synthesized (LHsExpr GhcPs))
hole = Synthesized (LHsExpr GhcPs)
-> ExtractM (Synthesized (LHsExpr GhcPs))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Synthesized (LHsExpr GhcPs)
-> ExtractM (Synthesized (LHsExpr GhcPs)))
-> (HsExpr GhcPs -> Synthesized (LHsExpr GhcPs))
-> HsExpr GhcPs
-> ExtractM (Synthesized (LHsExpr GhcPs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> ExtractM (Synthesized (LHsExpr GhcPs)))
-> HsExpr GhcPs -> ExtractM (Synthesized (LHsExpr GhcPs))
forall a b. (a -> b) -> a -> b
$ RdrNameStr -> HsExpr GhcPs
forall a. Var a => RdrNameStr -> a
var RdrNameStr
"_"
data TacticError
= UndefinedHypothesis OccName
| GoalMismatch String CType
| UnsolvedSubgoals [Judgement]
| UnificationError CType CType
| NoProgress
| NoApplicableTactic
| IncorrectDataCon DataCon
| RecursionOnWrongParam OccName Int OccName
| UnhelpfulDestruct OccName
| UnhelpfulSplit OccName
| TooPolymorphic
| NotInScope OccName
deriving stock (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 (UndefinedHypothesis OccName
name) =
OccName -> String
occNameString OccName
name String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" is not available in the hypothesis."
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 (UnsolvedSubgoals [Judgement]
_) =
String
"There were unsolved subgoals"
show (UnificationError (CType Type
t1) (CType Type
t2)) =
[String] -> String
forall a. Monoid a => [a] -> a
mconcat
[ String
"Could not unify "
, Type -> String
forall a. Outputable a => a -> String
unsafeRender Type
t1
, String
" and "
, Type -> String
forall a. Outputable a => a -> String
unsafeRender Type
t2
]
show TacticError
NoProgress =
String
"Unable to make progress"
show TacticError
NoApplicableTactic =
String
"No tactic could be applied"
show (IncorrectDataCon DataCon
dcon) =
String
"Data con doesn't align with goal type (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> DataCon -> String
forall a. Outputable a => a -> String
unsafeRender DataCon
dcon String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
show (RecursionOnWrongParam OccName
call Int
p OccName
arg) =
String
"Recursion on wrong param (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
call String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
") on arg"
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
p String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
": " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> OccName -> String
forall a. Show a => a -> String
show OccName
arg
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 (UnhelpfulSplit OccName
n) =
String
"Splitting constructor " 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 goals"
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
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
data Synthesized a = Synthesized
{ Synthesized a -> Trace
syn_trace :: Trace
, Synthesized a -> Hypothesis CType
syn_scoped :: Hypothesis CType
, Synthesized a -> Set OccName
syn_used_vals :: Set OccName
, Synthesized a -> Sum Int
syn_recursion_count :: Sum Int
, Synthesized a -> a
syn_val :: a
}
deriving (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)
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
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
data Context = Context
{ Context -> [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
, Context -> [(OccName, CType)]
ctxModuleFuncs :: [(OccName, CType)]
, Context -> FeatureSet
ctxFeatureSet :: FeatureSet
, Context -> KnownThings
ctxKnownThings :: KnownThings
, Context -> InstEnvs
ctxInstEnvs :: InstEnvs
, Context -> Set CType
ctxTheta :: Set CType
}
instance Show Context where
show :: Context -> String
show (Context {[(OccName, CType)]
FeatureSet
Set CType
InstEnvs
KnownThings
ctxTheta :: Set CType
ctxInstEnvs :: InstEnvs
ctxKnownThings :: KnownThings
ctxFeatureSet :: FeatureSet
ctxModuleFuncs :: [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
ctxTheta :: Context -> Set CType
ctxInstEnvs :: Context -> InstEnvs
ctxKnownThings :: Context -> KnownThings
ctxFeatureSet :: Context -> FeatureSet
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 -> FeatureSet -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 FeatureSet
ctxFeatureSet String
""
, Int -> Set CType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Set CType
ctxTheta String
""
]
data KnownThings = KnownThings
{ KnownThings -> Class
kt_semigroup :: Class
, KnownThings -> Class
kt_monoid :: Class
}
emptyContext :: Context
emptyContext :: Context
emptyContext
= Context :: [(OccName, CType)]
-> [(OccName, CType)]
-> FeatureSet
-> KnownThings
-> InstEnvs
-> Set CType
-> 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
, ctxFeatureSet :: FeatureSet
ctxFeatureSet = FeatureSet
forall a. Monoid a => a
mempty
, ctxKnownThings :: KnownThings
ctxKnownThings = String -> KnownThings
forall a. HasCallStack => String -> a
error String
"empty known things from emptyContext"
, 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
}
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)
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
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
data RunTacticResults = RunTacticResults
{ RunTacticResults -> Trace
rtr_trace :: Trace
, :: LHsExpr GhcPs
, RunTacticResults -> [Synthesized (LHsExpr GhcPs)]
rtr_other_solns :: [Synthesized (LHsExpr GhcPs)]
, RunTacticResults -> Judgement
rtr_jdg :: Judgement
, RunTacticResults -> Context
rtr_ctx :: Context
} 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
= 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
TacticErrors = String
"Wingman couldn't find a solution"
show UserFacingMessage
TimedOut = String
"Wingman timed out while trying to find a solution"
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