{-# LANGUAGE OverloadedStrings #-}

module Ide.Plugin.Tactic.TestTypes where

import qualified Data.Text as T

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

-- | Generate a title for the command.
tacticTitle :: TacticCommand -> T.Text -> T.Text
tacticTitle :: TacticCommand -> Text -> Text
tacticTitle TacticCommand
Auto Text
_ = Text
"Attempt to fill hole"
tacticTitle TacticCommand
Intros Text
_ = Text
"Introduce lambda"
tacticTitle TacticCommand
Destruct Text
var = Text
"Case split on " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
var
tacticTitle TacticCommand
Homomorphism Text
var = Text
"Homomorphic case split on " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
var
tacticTitle TacticCommand
DestructLambdaCase Text
_ = Text
"Lambda case split"
tacticTitle TacticCommand
HomomorphismLambdaCase Text
_ = Text
"Homomorphic lambda case split"