{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Ide.Plugin.Tactic.Types
( module Ide.Plugin.Tactic.Types
, module Ide.Plugin.Tactic.Debug
, OccName
, Name
, Type
, TyVar
, Span
, Range
) where
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.Set (Set)
import Data.Tree
import Development.IDE.GHC.Compat hiding (Node)
import Development.IDE.GHC.Orphans ()
import Development.IDE.Types.Location
import GHC.Generics
import Ide.Plugin.Tactic.Debug
import Ide.Plugin.Tactic.FeatureSet (FeatureSet)
import OccName
import Refinery.Tactic
import System.IO.Unsafe (unsafePerformIO)
import Type
import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
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 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 (Pat GhcPs) where
show :: Pat GhcPs -> String
show = Pat GhcPs -> String
forall a. Outputable a => a -> String
unsafeRender
data TacticState = TacticState
{ TacticState -> Set Var
ts_skolems :: !(Set TyVar)
, TacticState -> TCvSubst
ts_unifier :: !TCvSubst
, TacticState -> Set OccName
ts_used_vals :: !(Set OccName)
, TacticState -> Set OccName
ts_intro_vals :: !(Set OccName)
, TacticState -> Set OccName
ts_unused_top_vals :: !(Set OccName)
, TacticState -> [Maybe PatVal]
ts_recursion_stack :: ![Maybe PatVal]
, TacticState -> Int
ts_recursion_count :: !Int
, 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
-> Set OccName
-> Set OccName
-> Set OccName
-> [Maybe PatVal]
-> Int
-> 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_used_vals :: Set OccName
ts_used_vals = Set OccName
forall a. Monoid a => a
mempty
, ts_intro_vals :: Set OccName
ts_intro_vals = Set OccName
forall a. Monoid a => a
mempty
, ts_unused_top_vals :: Set OccName
ts_unused_top_vals = Set OccName
forall a. Monoid a => a
mempty
, ts_recursion_stack :: [Maybe PatVal]
ts_recursion_stack = [Maybe PatVal]
forall a. Monoid a => a
mempty
, ts_recursion_count :: Int
ts_recursion_count = Int
0
, 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
withRecursionStack
:: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
withRecursionStack :: ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
withRecursionStack [Maybe PatVal] -> [Maybe PatVal]
f =
forall s t a b.
HasField "ts_recursion_stack" 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_recursion_stack" (([Maybe PatVal] -> Identity [Maybe PatVal])
-> TacticState -> Identity TacticState)
-> ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ [Maybe PatVal] -> [Maybe PatVal]
f
pushRecursionStack :: TacticState -> TacticState
pushRecursionStack :: TacticState -> TacticState
pushRecursionStack = ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
withRecursionStack (Maybe PatVal
forall a. Maybe a
Nothing Maybe PatVal -> [Maybe PatVal] -> [Maybe PatVal]
forall a. a -> [a] -> [a]
:)
popRecursionStack :: TacticState -> TacticState
popRecursionStack :: TacticState -> TacticState
popRecursionStack = ([Maybe PatVal] -> [Maybe PatVal]) -> TacticState -> TacticState
withRecursionStack [Maybe PatVal] -> [Maybe PatVal]
forall a. [a] -> [a]
tail
withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
withUsedVals Set OccName -> Set OccName
f =
forall s t a b. HasField "ts_used_vals" 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_used_vals" ((Set OccName -> Identity (Set OccName))
-> TacticState -> Identity TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Set OccName -> Set OccName
f
withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
withIntroducedVals Set OccName -> Set OccName
f =
forall s t a b. HasField "ts_intro_vals" 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_intro_vals" ((Set OccName -> Identity (Set OccName))
-> TacticState -> Identity TacticState)
-> (Set OccName -> Set OccName) -> TacticState -> TacticState
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Set OccName -> Set OccName
f
data Provenance
=
TopLevelArgPrv
OccName
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 DataCon
pv_datacon :: Uniquely DataCon
, 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 (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 (Trace, LHsExpr GhcPs) ExtractM where
hole :: ExtractM (Trace, LHsExpr GhcPs)
hole = (Trace, LHsExpr GhcPs) -> ExtractM (Trace, LHsExpr GhcPs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Trace
forall a. Monoid a => a
mempty, SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs)
-> SrcSpanLess (LHsExpr GhcPs) -> LHsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ XVar GhcPs -> Located (IdP GhcPs) -> HsExpr GhcPs
forall p. XVar p -> Located (IdP p) -> HsExpr p
HsVar NoExtField
XVar GhcPs
noExtField (Located (IdP GhcPs) -> HsExpr GhcPs)
-> Located (IdP GhcPs) -> HsExpr GhcPs
forall a b. (a -> b) -> a -> b
$ SrcSpanLess (Located RdrName) -> Located RdrName
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (SrcSpanLess (Located RdrName) -> Located RdrName)
-> SrcSpanLess (Located RdrName) -> Located RdrName
forall a b. (a -> b) -> a -> b
$ OccName -> RdrName
Unqual (OccName -> RdrName) -> OccName -> RdrName
forall a b. (a -> b) -> a -> b
$ String -> OccName
mkVarOcc String
"_")
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 (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
type RuleM = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
type Rule = RuleM (Trace, LHsExpr GhcPs)
type Trace = Rose String
data Context = Context
{ Context -> [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
, Context -> [(OccName, CType)]
ctxModuleFuncs :: [(OccName, CType)]
, Context -> FeatureSet
ctxFeatureSet :: FeatureSet
}
deriving stock (Context -> Context -> Bool
(Context -> Context -> Bool)
-> (Context -> Context -> Bool) -> Eq Context
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Context -> Context -> Bool
$c/= :: Context -> Context -> Bool
== :: Context -> Context -> Bool
$c== :: Context -> Context -> Bool
Eq, Eq Context
Eq Context
-> (Context -> Context -> Ordering)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Bool)
-> (Context -> Context -> Context)
-> (Context -> Context -> Context)
-> Ord Context
Context -> Context -> Bool
Context -> Context -> Ordering
Context -> Context -> Context
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 :: Context -> Context -> Context
$cmin :: Context -> Context -> Context
max :: Context -> Context -> Context
$cmax :: Context -> Context -> Context
>= :: Context -> Context -> Bool
$c>= :: Context -> Context -> Bool
> :: Context -> Context -> Bool
$c> :: Context -> Context -> Bool
<= :: Context -> Context -> Bool
$c<= :: Context -> Context -> Bool
< :: Context -> Context -> Bool
$c< :: Context -> Context -> Bool
compare :: Context -> Context -> Ordering
$ccompare :: Context -> Context -> Ordering
$cp1Ord :: Eq Context
Ord, Int -> Context -> ShowS
[Context] -> ShowS
Context -> String
(Int -> Context -> ShowS)
-> (Context -> String) -> ([Context] -> ShowS) -> Show Context
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Context] -> ShowS
$cshowList :: [Context] -> ShowS
show :: Context -> String
$cshow :: Context -> String
showsPrec :: Int -> Context -> ShowS
$cshowsPrec :: Int -> Context -> ShowS
Show)
emptyContext :: Context
emptyContext :: Context
emptyContext = [(OccName, CType)] -> [(OccName, CType)] -> FeatureSet -> Context
Context [(OccName, CType)]
forall a. Monoid a => a
mempty [(OccName, CType)]
forall a. Monoid a => a
mempty FeatureSet
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 Semigroup 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)
instance 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 -> [(Trace, LHsExpr GhcPs)]
rtr_other_solns :: [(Trace, 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)