{-# 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)


------------------------------------------------------------------------------
-- | A wrapper around 'Type' which supports equality and ordering.
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)
      -- ^ The known skolems.
    , TacticState -> TCvSubst
ts_unifier   :: !TCvSubst
      -- ^ The current substitution of univars.
    , TacticState -> Set OccName
ts_used_vals :: !(Set OccName)
      -- ^ Set of values used by tactics.
    , TacticState -> Set OccName
ts_intro_vals :: !(Set OccName)
      -- ^ Set of values introduced by tactics.
    , TacticState -> Set OccName
ts_unused_top_vals :: !(Set OccName)
      -- ^ Set of currently unused arguments to the function being defined.
    , TacticState -> [Maybe PatVal]
ts_recursion_stack :: ![Maybe PatVal]
      -- ^ Stack for tracking whether or not the current recursive call has
      -- used at least one smaller pat val. Recursive calls for which this
      -- value is 'False' are guaranteed to loop, and must be pruned.
    , TacticState -> Int
ts_recursion_count :: !Int
      -- ^ Number of calls to recursion. We penalize each.
    , TacticState -> UniqSupply
ts_unique_gen :: !UniqSupply
    } deriving stock (Int -> TacticState -> ShowS
[TacticState] -> ShowS
TacticState -> String
(Int -> TacticState -> ShowS)
-> (TacticState -> String)
-> ([TacticState] -> ShowS)
-> Show TacticState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TacticState] -> ShowS
$cshowList :: [TacticState] -> ShowS
show :: TacticState -> String
$cshow :: TacticState -> String
showsPrec :: Int -> TacticState -> ShowS
$cshowsPrec :: Int -> TacticState -> ShowS
Show, (forall x. TacticState -> Rep TacticState x)
-> (forall x. Rep TacticState x -> TacticState)
-> Generic TacticState
forall x. Rep TacticState x -> TacticState
forall x. TacticState -> Rep TacticState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TacticState x -> TacticState
$cfrom :: forall x. TacticState -> Rep TacticState x
Generic)

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


------------------------------------------------------------------------------
-- | A 'UniqSupply' to use in 'defaultTacticState'
unsafeDefaultUniqueSupply :: UniqSupply
unsafeDefaultUniqueSupply :: UniqSupply
unsafeDefaultUniqueSupply =
  IO UniqSupply -> UniqSupply
forall a. IO a -> a
unsafePerformIO (IO UniqSupply -> UniqSupply) -> IO UniqSupply -> UniqSupply
forall a b. (a -> b) -> a -> b
$ Char -> IO UniqSupply
mkSplitUniqSupply Char
'🚒'
{-# 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
    }


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


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


------------------------------------------------------------------------------
-- | Describes where hypotheses came from. Used extensively to prune stupid
-- solutions from the search space.
data Provenance
  = -- | An argument given to the topmost function that contains the current
    -- hole. Recursive calls are restricted to values whose provenance lines up
    -- with the same argument.
    TopLevelArgPrv
      OccName   -- ^ Binding function
      Int       -- ^ Argument Position
    -- | A binding created in a pattern match.
  | PatternMatchPrv PatVal
    -- | A class method from the given context.
  | ClassMethodPrv
      (Uniquely Class)     -- ^ Class
    -- | A binding explicitly written by the user.
  | UserPrv
    -- | The recursive hypothesis. Present only in the context of the recursion
    -- tactic.
  | RecursivePrv
    -- | A hypothesis which has been disallowed for some reason. It's important
    -- to keep these in the hypothesis set, rather than filtering it, in order
    -- to continue tracking downstream provenance.
  | DisallowedPrv DisallowReason Provenance
  deriving stock (Provenance -> Provenance -> Bool
(Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool) -> Eq Provenance
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Provenance -> Provenance -> Bool
$c/= :: Provenance -> Provenance -> Bool
== :: Provenance -> Provenance -> Bool
$c== :: Provenance -> Provenance -> Bool
Eq, Int -> Provenance -> ShowS
[Provenance] -> ShowS
Provenance -> String
(Int -> Provenance -> ShowS)
-> (Provenance -> String)
-> ([Provenance] -> ShowS)
-> Show Provenance
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Provenance] -> ShowS
$cshowList :: [Provenance] -> ShowS
show :: Provenance -> String
$cshow :: Provenance -> String
showsPrec :: Int -> Provenance -> ShowS
$cshowsPrec :: Int -> Provenance -> ShowS
Show, (forall x. Provenance -> Rep Provenance x)
-> (forall x. Rep Provenance x -> Provenance) -> Generic Provenance
forall x. Rep Provenance x -> Provenance
forall x. Provenance -> Rep Provenance x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Provenance x -> Provenance
$cfrom :: forall x. Provenance -> Rep Provenance x
Generic, Eq Provenance
Eq Provenance
-> (Provenance -> Provenance -> Ordering)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Provenance)
-> (Provenance -> Provenance -> Provenance)
-> Ord Provenance
Provenance -> Provenance -> Bool
Provenance -> Provenance -> Ordering
Provenance -> Provenance -> Provenance
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Provenance -> Provenance -> Provenance
$cmin :: Provenance -> Provenance -> Provenance
max :: Provenance -> Provenance -> Provenance
$cmax :: Provenance -> Provenance -> Provenance
>= :: Provenance -> Provenance -> Bool
$c>= :: Provenance -> Provenance -> Bool
> :: Provenance -> Provenance -> Bool
$c> :: Provenance -> Provenance -> Bool
<= :: Provenance -> Provenance -> Bool
$c<= :: Provenance -> Provenance -> Bool
< :: Provenance -> Provenance -> Bool
$c< :: Provenance -> Provenance -> Bool
compare :: Provenance -> Provenance -> Ordering
$ccompare :: Provenance -> Provenance -> Ordering
$cp1Ord :: Eq Provenance
Ord)


------------------------------------------------------------------------------
-- | Why was a hypothesis disallowed?
data DisallowReason
  = WrongBranch Int
  | Shadowed
  | RecursiveCall
  | AlreadyDestructed
  deriving stock (DisallowReason -> DisallowReason -> Bool
(DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool) -> Eq DisallowReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DisallowReason -> DisallowReason -> Bool
$c/= :: DisallowReason -> DisallowReason -> Bool
== :: DisallowReason -> DisallowReason -> Bool
$c== :: DisallowReason -> DisallowReason -> Bool
Eq, Int -> DisallowReason -> ShowS
[DisallowReason] -> ShowS
DisallowReason -> String
(Int -> DisallowReason -> ShowS)
-> (DisallowReason -> String)
-> ([DisallowReason] -> ShowS)
-> Show DisallowReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DisallowReason] -> ShowS
$cshowList :: [DisallowReason] -> ShowS
show :: DisallowReason -> String
$cshow :: DisallowReason -> String
showsPrec :: Int -> DisallowReason -> ShowS
$cshowsPrec :: Int -> DisallowReason -> ShowS
Show, (forall x. DisallowReason -> Rep DisallowReason x)
-> (forall x. Rep DisallowReason x -> DisallowReason)
-> Generic DisallowReason
forall x. Rep DisallowReason x -> DisallowReason
forall x. DisallowReason -> Rep DisallowReason x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DisallowReason x -> DisallowReason
$cfrom :: forall x. DisallowReason -> Rep DisallowReason x
Generic, Eq DisallowReason
Eq DisallowReason
-> (DisallowReason -> DisallowReason -> Ordering)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> Bool)
-> (DisallowReason -> DisallowReason -> DisallowReason)
-> (DisallowReason -> DisallowReason -> DisallowReason)
-> Ord DisallowReason
DisallowReason -> DisallowReason -> Bool
DisallowReason -> DisallowReason -> Ordering
DisallowReason -> DisallowReason -> DisallowReason
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DisallowReason -> DisallowReason -> DisallowReason
$cmin :: DisallowReason -> DisallowReason -> DisallowReason
max :: DisallowReason -> DisallowReason -> DisallowReason
$cmax :: DisallowReason -> DisallowReason -> DisallowReason
>= :: DisallowReason -> DisallowReason -> Bool
$c>= :: DisallowReason -> DisallowReason -> Bool
> :: DisallowReason -> DisallowReason -> Bool
$c> :: DisallowReason -> DisallowReason -> Bool
<= :: DisallowReason -> DisallowReason -> Bool
$c<= :: DisallowReason -> DisallowReason -> Bool
< :: DisallowReason -> DisallowReason -> Bool
$c< :: DisallowReason -> DisallowReason -> Bool
compare :: DisallowReason -> DisallowReason -> Ordering
$ccompare :: DisallowReason -> DisallowReason -> Ordering
$cp1Ord :: Eq DisallowReason
Ord)


------------------------------------------------------------------------------
-- | Provenance of a pattern value.
data PatVal = PatVal
  { PatVal -> Maybe OccName
pv_scrutinee :: Maybe OccName
    -- ^ Original scrutinee which created this PatVal. Nothing, for lambda
    -- case.
  , PatVal -> Set OccName
pv_ancestry  :: Set OccName
    -- ^ The set of values which had to be destructed to discover this term.
    -- Always contains the scrutinee.
  , PatVal -> Uniquely DataCon
pv_datacon   :: Uniquely DataCon
    -- ^ The datacon which introduced this term.
  , PatVal -> Int
pv_position  :: Int
    -- ^ The position of this binding in the datacon's arguments.
  } deriving stock (PatVal -> PatVal -> Bool
(PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool) -> Eq PatVal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatVal -> PatVal -> Bool
$c/= :: PatVal -> PatVal -> Bool
== :: PatVal -> PatVal -> Bool
$c== :: PatVal -> PatVal -> Bool
Eq, Int -> PatVal -> ShowS
[PatVal] -> ShowS
PatVal -> String
(Int -> PatVal -> ShowS)
-> (PatVal -> String) -> ([PatVal] -> ShowS) -> Show PatVal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PatVal] -> ShowS
$cshowList :: [PatVal] -> ShowS
show :: PatVal -> String
$cshow :: PatVal -> String
showsPrec :: Int -> PatVal -> ShowS
$cshowsPrec :: Int -> PatVal -> ShowS
Show, (forall x. PatVal -> Rep PatVal x)
-> (forall x. Rep PatVal x -> PatVal) -> Generic PatVal
forall x. Rep PatVal x -> PatVal
forall x. PatVal -> Rep PatVal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PatVal x -> PatVal
$cfrom :: forall x. PatVal -> Rep PatVal x
Generic, Eq PatVal
Eq PatVal
-> (PatVal -> PatVal -> Ordering)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> Bool)
-> (PatVal -> PatVal -> PatVal)
-> (PatVal -> PatVal -> PatVal)
-> Ord PatVal
PatVal -> PatVal -> Bool
PatVal -> PatVal -> Ordering
PatVal -> PatVal -> PatVal
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PatVal -> PatVal -> PatVal
$cmin :: PatVal -> PatVal -> PatVal
max :: PatVal -> PatVal -> PatVal
$cmax :: PatVal -> PatVal -> PatVal
>= :: PatVal -> PatVal -> Bool
$c>= :: PatVal -> PatVal -> Bool
> :: PatVal -> PatVal -> Bool
$c> :: PatVal -> PatVal -> Bool
<= :: PatVal -> PatVal -> Bool
$c<= :: PatVal -> PatVal -> Bool
< :: PatVal -> PatVal -> Bool
$c< :: PatVal -> PatVal -> Bool
compare :: PatVal -> PatVal -> Ordering
$ccompare :: PatVal -> PatVal -> Ordering
$cp1Ord :: Eq PatVal
Ord)


------------------------------------------------------------------------------
-- | A wrapper which uses a 'Uniquable' constraint for providing 'Eq' and 'Ord'
-- instances.
newtype Uniquely a = Uniquely { Uniquely a -> a
getViaUnique :: a }
  deriving Int -> Uniquely a -> ShowS
[Uniquely a] -> ShowS
Uniquely a -> String
(Int -> Uniquely a -> ShowS)
-> (Uniquely a -> String)
-> ([Uniquely a] -> ShowS)
-> Show (Uniquely a)
forall a. Show a => Int -> Uniquely a -> ShowS
forall a. Show a => [Uniquely a] -> ShowS
forall a. Show a => Uniquely a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Uniquely a] -> ShowS
$cshowList :: forall a. Show a => [Uniquely a] -> ShowS
show :: Uniquely a -> String
$cshow :: forall a. Show a => Uniquely a -> String
showsPrec :: Int -> Uniquely a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Uniquely a -> ShowS
Show via a

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)


------------------------------------------------------------------------------
-- | The provenance and type of a hypothesis term.
data HyInfo a = HyInfo
  { HyInfo a -> OccName
hi_name       :: OccName
  , HyInfo a -> Provenance
hi_provenance :: Provenance
  , HyInfo a -> a
hi_type       :: a
  }
  deriving stock (a -> HyInfo b -> HyInfo a
(a -> b) -> HyInfo a -> HyInfo b
(forall a b. (a -> b) -> HyInfo a -> HyInfo b)
-> (forall a b. a -> HyInfo b -> HyInfo a) -> Functor HyInfo
forall a b. a -> HyInfo b -> HyInfo a
forall a b. (a -> b) -> HyInfo a -> HyInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> HyInfo b -> HyInfo a
$c<$ :: forall a b. a -> HyInfo b -> HyInfo a
fmap :: (a -> b) -> HyInfo a -> HyInfo b
$cfmap :: forall a b. (a -> b) -> HyInfo a -> HyInfo b
Functor, HyInfo a -> HyInfo a -> Bool
(HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool) -> Eq (HyInfo a)
forall a. Eq a => HyInfo a -> HyInfo a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HyInfo a -> HyInfo a -> Bool
$c/= :: forall a. Eq a => HyInfo a -> HyInfo a -> Bool
== :: HyInfo a -> HyInfo a -> Bool
$c== :: forall a. Eq a => HyInfo a -> HyInfo a -> Bool
Eq, Int -> HyInfo a -> ShowS
[HyInfo a] -> ShowS
HyInfo a -> String
(Int -> HyInfo a -> ShowS)
-> (HyInfo a -> String) -> ([HyInfo a] -> ShowS) -> Show (HyInfo a)
forall a. Show a => Int -> HyInfo a -> ShowS
forall a. Show a => [HyInfo a] -> ShowS
forall a. Show a => HyInfo a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HyInfo a] -> ShowS
$cshowList :: forall a. Show a => [HyInfo a] -> ShowS
show :: HyInfo a -> String
$cshow :: forall a. Show a => HyInfo a -> String
showsPrec :: Int -> HyInfo a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> HyInfo a -> ShowS
Show, (forall x. HyInfo a -> Rep (HyInfo a) x)
-> (forall x. Rep (HyInfo a) x -> HyInfo a) -> Generic (HyInfo a)
forall x. Rep (HyInfo a) x -> HyInfo a
forall x. HyInfo a -> Rep (HyInfo a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (HyInfo a) x -> HyInfo a
forall a x. HyInfo a -> Rep (HyInfo a) x
$cto :: forall a x. Rep (HyInfo a) x -> HyInfo a
$cfrom :: forall a x. HyInfo a -> Rep (HyInfo a) x
Generic, Eq (HyInfo a)
Eq (HyInfo a)
-> (HyInfo a -> HyInfo a -> Ordering)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> Bool)
-> (HyInfo a -> HyInfo a -> HyInfo a)
-> (HyInfo a -> HyInfo a -> HyInfo a)
-> Ord (HyInfo a)
HyInfo a -> HyInfo a -> Bool
HyInfo a -> HyInfo a -> Ordering
HyInfo a -> HyInfo a -> HyInfo a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (HyInfo a)
forall a. Ord a => HyInfo a -> HyInfo a -> Bool
forall a. Ord a => HyInfo a -> HyInfo a -> Ordering
forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
min :: HyInfo a -> HyInfo a -> HyInfo a
$cmin :: forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
max :: HyInfo a -> HyInfo a -> HyInfo a
$cmax :: forall a. Ord a => HyInfo a -> HyInfo a -> HyInfo a
>= :: HyInfo a -> HyInfo a -> Bool
$c>= :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
> :: HyInfo a -> HyInfo a -> Bool
$c> :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
<= :: HyInfo a -> HyInfo a -> Bool
$c<= :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
< :: HyInfo a -> HyInfo a -> Bool
$c< :: forall a. Ord a => HyInfo a -> HyInfo a -> Bool
compare :: HyInfo a -> HyInfo a -> Ordering
$ccompare :: forall a. Ord a => HyInfo a -> HyInfo a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (HyInfo a)
Ord)


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


------------------------------------------------------------------------------
-- | The current bindings and goal for a hole to be filled by refinery.
data Judgement' a = Judgement
  { Judgement' a -> Hypothesis a
_jHypothesis :: !(Hypothesis a)
  , Judgement' a -> Bool
_jBlacklistDestruct :: !Bool
  , Judgement' a -> Bool
_jWhitelistSplit :: !Bool
  , Judgement' a -> Bool
_jIsTopHole    :: !Bool
  , Judgement' a -> a
_jGoal         :: !a
  }
  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 ExtractM a = ExtractM { ExtractM a -> Reader Context a
unExtractM :: 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)

------------------------------------------------------------------------------
-- | Orphan instance for producing holes when attempting to solve tactics.
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
"_")


------------------------------------------------------------------------------
-- | Reasons a tactic might fail.
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


------------------------------------------------------------------------------
-- | The Reader context of tactics and rules
data Context = Context
  { Context -> [(OccName, CType)]
ctxDefiningFuncs :: [(OccName, CType)]
    -- ^ The functions currently being defined
  , Context -> [(OccName, CType)]
ctxModuleFuncs :: [(OccName, CType)]
    -- ^ Everything defined in the current module
  , Context -> 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)


------------------------------------------------------------------------------
-- | An empty context
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


------------------------------------------------------------------------------
-- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic'
data RunTacticResults = RunTacticResults
  { RunTacticResults -> Trace
rtr_trace       :: Trace
  , RunTacticResults -> LHsExpr GhcPs
rtr_extract     :: 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)