{-# LANGUAGE CPP               #-}
{-# LANGUAGE NamedFieldPuns    #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-deprecations #-}

module Wingman.Metaprogramming.ProofState where

import           Data.Bool (bool)
import           Data.Functor ((<&>))
import qualified Data.Text as T
import           Data.Text.Prettyprint.Doc
import           Data.Text.Prettyprint.Doc.Render.Util.Panic
import           Language.LSP.Types (sectionSeparator)
import           Wingman.Judgements (jHypothesis)
import           Wingman.Types

renderSimplyDecorated
    :: Monoid out
    => (T.Text -> out) -- ^ Render plain 'Text'
    -> (ann -> out)  -- ^ How to render an annotation
    -> (ann -> out)  -- ^ How to render the removed annotation
    -> SimpleDocStream ann
    -> out
renderSimplyDecorated :: (Text -> out)
-> (ann -> out) -> (ann -> out) -> SimpleDocStream ann -> out
renderSimplyDecorated Text -> out
text ann -> out
push ann -> out
pop = [ann] -> SimpleDocStream ann -> out
go []
  where
    go :: [ann] -> SimpleDocStream ann -> out
go [ann]
_        SimpleDocStream ann
SFail               = out
forall void. void
panicUncaughtFail
    go []       SimpleDocStream ann
SEmpty              = out
forall a. Monoid a => a
mempty
    go (ann
_:[ann]
_)    SimpleDocStream ann
SEmpty              = out
forall void. void
panicInputNotFullyConsumed
    go [ann]
st       (SChar Char
c SimpleDocStream ann
rest)      = Text -> out
text (Char -> Text
T.singleton Char
c) out -> out -> out
forall a. Semigroup a => a -> a -> a
<> [ann] -> SimpleDocStream ann -> out
go [ann]
st SimpleDocStream ann
rest
    go [ann]
st       (SText Int
_l Text
t SimpleDocStream ann
rest)   = Text -> out
text Text
t out -> out -> out
forall a. Semigroup a => a -> a -> a
<> [ann] -> SimpleDocStream ann -> out
go [ann]
st SimpleDocStream ann
rest
    go [ann]
st       (SLine Int
i SimpleDocStream ann
rest)      =
      Text -> out
text (Char -> Text
T.singleton Char
'\n') out -> out -> out
forall a. Semigroup a => a -> a -> a
<> Text -> out
text (Int -> Text
textSpaces Int
i) out -> out -> out
forall a. Semigroup a => a -> a -> a
<> [ann] -> SimpleDocStream ann -> out
go [ann]
st SimpleDocStream ann
rest
    go [ann]
st       (SAnnPush ann
ann SimpleDocStream ann
rest) = ann -> out
push ann
ann out -> out -> out
forall a. Semigroup a => a -> a -> a
<> [ann] -> SimpleDocStream ann -> out
go (ann
ann ann -> [ann] -> [ann]
forall a. a -> [a] -> [a]
: [ann]
st) SimpleDocStream ann
rest
    go (ann
ann:[ann]
st) (SAnnPop SimpleDocStream ann
rest)      = ann -> out
pop ann
ann out -> out -> out
forall a. Semigroup a => a -> a -> a
<> [ann] -> SimpleDocStream ann -> out
go [ann]
st SimpleDocStream ann
rest
    go []       SAnnPop{}           = out
forall void. void
panicUnpairedPop
{-# INLINE renderSimplyDecorated #-}


data Ann
  = Goal
  | Hypoth
  | Status
  deriving (Ann -> Ann -> Bool
(Ann -> Ann -> Bool) -> (Ann -> Ann -> Bool) -> Eq Ann
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ann -> Ann -> Bool
$c/= :: Ann -> Ann -> Bool
== :: Ann -> Ann -> Bool
$c== :: Ann -> Ann -> Bool
Eq, Eq Ann
Eq Ann
-> (Ann -> Ann -> Ordering)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Bool)
-> (Ann -> Ann -> Ann)
-> (Ann -> Ann -> Ann)
-> Ord Ann
Ann -> Ann -> Bool
Ann -> Ann -> Ordering
Ann -> Ann -> Ann
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 :: Ann -> Ann -> Ann
$cmin :: Ann -> Ann -> Ann
max :: Ann -> Ann -> Ann
$cmax :: Ann -> Ann -> Ann
>= :: Ann -> Ann -> Bool
$c>= :: Ann -> Ann -> Bool
> :: Ann -> Ann -> Bool
$c> :: Ann -> Ann -> Bool
<= :: Ann -> Ann -> Bool
$c<= :: Ann -> Ann -> Bool
< :: Ann -> Ann -> Bool
$c< :: Ann -> Ann -> Bool
compare :: Ann -> Ann -> Ordering
$ccompare :: Ann -> Ann -> Ordering
$cp1Ord :: Eq Ann
Ord, Int -> Ann -> ShowS
[Ann] -> ShowS
Ann -> String
(Int -> Ann -> ShowS)
-> (Ann -> String) -> ([Ann] -> ShowS) -> Show Ann
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ann] -> ShowS
$cshowList :: [Ann] -> ShowS
show :: Ann -> String
$cshow :: Ann -> String
showsPrec :: Int -> Ann -> ShowS
$cshowsPrec :: Int -> Ann -> ShowS
Show, Int -> Ann
Ann -> Int
Ann -> [Ann]
Ann -> Ann
Ann -> Ann -> [Ann]
Ann -> Ann -> Ann -> [Ann]
(Ann -> Ann)
-> (Ann -> Ann)
-> (Int -> Ann)
-> (Ann -> Int)
-> (Ann -> [Ann])
-> (Ann -> Ann -> [Ann])
-> (Ann -> Ann -> [Ann])
-> (Ann -> Ann -> Ann -> [Ann])
-> Enum Ann
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 :: Ann -> Ann -> Ann -> [Ann]
$cenumFromThenTo :: Ann -> Ann -> Ann -> [Ann]
enumFromTo :: Ann -> Ann -> [Ann]
$cenumFromTo :: Ann -> Ann -> [Ann]
enumFromThen :: Ann -> Ann -> [Ann]
$cenumFromThen :: Ann -> Ann -> [Ann]
enumFrom :: Ann -> [Ann]
$cenumFrom :: Ann -> [Ann]
fromEnum :: Ann -> Int
$cfromEnum :: Ann -> Int
toEnum :: Int -> Ann
$ctoEnum :: Int -> Ann
pred :: Ann -> Ann
$cpred :: Ann -> Ann
succ :: Ann -> Ann
$csucc :: Ann -> Ann
Enum, Ann
Ann -> Ann -> Bounded Ann
forall a. a -> a -> Bounded a
maxBound :: Ann
$cmaxBound :: Ann
minBound :: Ann
$cminBound :: Ann
Bounded)

forceMarkdownNewlines :: String -> String
forceMarkdownNewlines :: ShowS
forceMarkdownNewlines = [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"  ") ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines

layout :: Bool -> Doc Ann -> String
layout :: Bool -> Doc Ann -> String
layout Bool
use_styling
  = ShowS
forceMarkdownNewlines
  ShowS -> (Doc Ann -> String) -> Doc Ann -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack
  (Text -> String) -> (Doc Ann -> Text) -> Doc Ann -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Text)
-> (Ann -> Text) -> (Ann -> Text) -> SimpleDocStream Ann -> Text
forall out ann.
Monoid out =>
(Text -> out)
-> (ann -> out) -> (ann -> out) -> SimpleDocStream ann -> out
renderSimplyDecorated Text -> Text
forall a. a -> a
id
    (Bool -> Ann -> Text
renderAnn Bool
use_styling)
    (Bool -> Ann -> Text
renderUnann Bool
use_styling)
  (SimpleDocStream Ann -> Text)
-> (Doc Ann -> SimpleDocStream Ann) -> Doc Ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Ann -> SimpleDocStream Ann
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty (PageWidth -> LayoutOptions
LayoutOptions (PageWidth -> LayoutOptions) -> PageWidth -> LayoutOptions
forall a b. (a -> b) -> a -> b
$ Int -> Double -> PageWidth
AvailablePerLine Int
80 Double
0.6)

renderAnn :: Bool -> Ann -> T.Text
renderAnn :: Bool -> Ann -> Text
renderAnn Bool
False Ann
_ = Text
""
renderAnn Bool
_ Ann
Goal = Text
"<span style='color:#ef4026;'>"
renderAnn Bool
_ Ann
Hypoth = Text
"```haskell\n"
renderAnn Bool
_ Ann
Status = Text
"<span style='color:#6495ED;'>"

renderUnann :: Bool -> Ann -> T.Text
renderUnann :: Bool -> Ann -> Text
renderUnann Bool
False Ann
_ = Text
""
renderUnann Bool
_ Ann
Goal = Text
"</span>"
renderUnann Bool
_ Ann
Hypoth = Text
"\n```\n"
renderUnann Bool
_ Ann
Status = Text
"</span>"

proofState :: RunTacticResults -> Doc Ann
proofState :: RunTacticResults -> Doc Ann
proofState RunTacticResults{[Judgement]
rtr_subgoals :: RunTacticResults -> [Judgement]
rtr_subgoals :: [Judgement]
rtr_subgoals} =
  [Doc Ann] -> Doc Ann
forall ann. [Doc ann] -> Doc ann
vsep
    ([Doc Ann] -> Doc Ann) -> [Doc Ann] -> Doc Ann
forall a b. (a -> b) -> a -> b
$ ( Ann -> Doc Ann -> Doc Ann
forall ann. ann -> Doc ann -> Doc ann
annotate Ann
Status
      (Doc Ann -> Doc Ann) -> (Int -> Doc Ann) -> Int -> Doc Ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Ann -> Doc Ann -> Int -> Doc Ann
countFinished Doc Ann
"goals accomplished 🎉" Doc Ann
"goal"
      (Int -> Doc Ann) -> Int -> Doc Ann
forall a b. (a -> b) -> a -> b
$ [Judgement] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Judgement]
rtr_subgoals
      )
    Doc Ann -> [Doc Ann] -> [Doc Ann]
forall a. a -> [a] -> [a]
: Text -> Doc Ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
sectionSeparator
    Doc Ann -> [Doc Ann] -> [Doc Ann]
forall a. a -> [a] -> [a]
: (Judgement -> Doc Ann) -> [Judgement] -> [Doc Ann]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Judgement -> Doc Ann
prettySubgoal [Judgement]
rtr_subgoals


prettySubgoal :: Judgement -> Doc Ann
prettySubgoal :: Judgement -> Doc Ann
prettySubgoal Judgement
jdg =
  [Doc Ann] -> Doc Ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc Ann] -> Doc Ann) -> [Doc Ann] -> Doc Ann
forall a b. (a -> b) -> a -> b
$
    [ Doc Ann
forall a. Monoid a => a
mempty | Bool
has_hy] [Doc Ann] -> [Doc Ann] -> [Doc Ann]
forall a. Semigroup a => a -> a -> a
<>
    [ Ann -> Doc Ann -> Doc Ann
forall ann. ann -> Doc ann -> Doc ann
annotate Ann
Hypoth (Doc Ann -> Doc Ann) -> Doc Ann -> Doc Ann
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Doc Ann
prettyHypothesis Hypothesis CType
hy | Bool
has_hy] [Doc Ann] -> [Doc Ann] -> [Doc Ann]
forall a. Semigroup a => a -> a -> a
<>
    [ Doc Ann
"⊢" Doc Ann -> Doc Ann -> Doc Ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Ann -> Doc Ann -> Doc Ann
forall ann. ann -> Doc ann -> Doc ann
annotate Ann
Goal (CType -> Doc Ann
prettyType (Judgement -> CType
forall a. Judgement' a -> a
_jGoal Judgement
jdg))
    , Text -> Doc Ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
sectionSeparator
    ]
  where
    hy :: Hypothesis CType
hy = Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg
    has_hy :: Bool
has_hy = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [HyInfo CType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([HyInfo CType] -> Bool) -> [HyInfo CType] -> Bool
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
hy


prettyHypothesis :: Hypothesis CType -> Doc Ann
prettyHypothesis :: Hypothesis CType -> Doc Ann
prettyHypothesis Hypothesis CType
hy =
  [Doc Ann] -> Doc Ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc Ann] -> Doc Ann) -> [Doc Ann] -> Doc Ann
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis CType
hy [HyInfo CType] -> (HyInfo CType -> Doc Ann) -> [Doc Ann]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \HyInfo CType
hi ->
    HyInfo CType -> Doc Ann
prettyHyInfo HyInfo CType
hi

prettyHyInfo :: HyInfo CType -> Doc Ann
prettyHyInfo :: HyInfo CType -> Doc Ann
prettyHyInfo HyInfo CType
hi = OccName -> Doc Ann
forall a ann. Show a => a -> Doc ann
viaShow (HyInfo CType -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo CType
hi) Doc Ann -> Doc Ann -> Doc Ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Ann
"::" Doc Ann -> Doc Ann -> Doc Ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> CType -> Doc Ann
prettyType (HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type HyInfo CType
hi)


prettyType :: CType -> Doc Ann
prettyType :: CType -> Doc Ann
prettyType (CType Type
ty) = Type -> Doc Ann
forall a ann. Show a => a -> Doc ann
viaShow Type
ty


countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann
countFinished :: Doc Ann -> Doc Ann -> Int -> Doc Ann
countFinished Doc Ann
finished Doc Ann
_ Int
0 = Doc Ann
finished
countFinished Doc Ann
_ Doc Ann
thing Int
n    = Doc Ann -> Int -> Doc Ann
count Doc Ann
thing Int
n

count :: Doc Ann -> Int -> Doc Ann
count :: Doc Ann -> Int -> Doc Ann
count Doc Ann
thing Int
n =
  Int -> Doc Ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
n Doc Ann -> Doc Ann -> Doc Ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Ann
thing Doc Ann -> Doc Ann -> Doc Ann
forall a. Semigroup a => a -> a -> a
<> Doc Ann -> Doc Ann -> Bool -> Doc Ann
forall a. a -> a -> Bool -> a
bool Doc Ann
"" Doc Ann
"s" (Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1)

textSpaces :: Int -> T.Text
textSpaces :: Int -> Text
textSpaces Int
n = Int -> Text -> Text
T.replicate Int
n (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Char -> Text
T.singleton Char
' '