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

module Wingman.Metaprogramming.Parser.Documentation where

import           Data.Functor ((<&>))
import           Data.List (sortOn)
import           Data.String (IsString)
import           Data.Text (Text)
import           Data.Text.Prettyprint.Doc hiding (parens)
import           Data.Text.Prettyprint.Doc.Render.String (renderString)
import           Development.IDE.GHC.Compat (OccName)
import qualified Text.Megaparsec as P
import           Wingman.Metaprogramming.Lexer (Parser, identifier, variable, parens)
import           Wingman.Types (TacticsM)

import {-# SOURCE #-} Wingman.Metaprogramming.Parser (tactic)


------------------------------------------------------------------------------
-- | Is a tactic deterministic or not?
data Determinism
  = Deterministic
  | Nondeterministic

prettyDeterminism :: Determinism -> Doc b
prettyDeterminism :: Determinism -> Doc b
prettyDeterminism Determinism
Deterministic = Doc b
"deterministic"
prettyDeterminism Determinism
Nondeterministic = Doc b
"non-deterministic"


------------------------------------------------------------------------------
-- | How many arguments does the tactic take?
data Count a where
  One  :: Count OccName
  Many :: Count [OccName]

prettyCount :: Count a -> Doc b
prettyCount :: Count a -> Doc b
prettyCount Count a
One  = Doc b
"single"
prettyCount Count a
Many = Doc b
"varadic"


------------------------------------------------------------------------------
-- | What sorts of arguments does the tactic take? Currently there is no
-- distincion between 'Ref' and 'Bind', other than documentation.
--
-- The type index here is used for the shape of the function the parser should
-- take.
data Syntax a where
  Nullary :: Syntax (Parser (TacticsM ()))
  Ref     :: Count a -> Syntax (a -> Parser (TacticsM ()))
  Bind    :: Count a -> Syntax (a -> Parser (TacticsM ()))
  Tactic  :: Syntax (TacticsM () -> Parser (TacticsM ()))

prettySyntax :: Syntax a -> Doc b
prettySyntax :: Syntax a -> Doc b
prettySyntax Syntax a
Nullary   = Doc b
"none"
prettySyntax (Ref Count a
co)  = Count a -> Doc b
forall a b. Count a -> Doc b
prettyCount Count a
co Doc b -> Doc b -> Doc b
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc b
"reference"
prettySyntax (Bind Count a
co) = Count a -> Doc b
forall a b. Count a -> Doc b
prettyCount Count a
co Doc b -> Doc b -> Doc b
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc b
"binding"
prettySyntax Syntax a
Tactic    = Doc b
"tactic"


------------------------------------------------------------------------------
-- | An example for the documentation.
data Example = Example
  { Example -> Maybe Text
ex_ctx    :: Maybe Text         -- ^ Specific context information about when the tactic is applicable
  , Example -> [Var]
ex_args   :: [Var]              -- ^ Arguments the tactic was called with
  , Example -> [ExampleHyInfo]
ex_hyp    :: [ExampleHyInfo]    -- ^ The hypothesis
  , Example -> Maybe ExampleType
ex_goal   :: Maybe ExampleType  -- ^ Current goal. Nothing indicates it's uninteresting.
  , Example -> Text
ex_result :: Text               -- ^ Resulting extract.
  }


------------------------------------------------------------------------------
-- | An example 'HyInfo'.
data ExampleHyInfo = EHI
  { ExampleHyInfo -> Var
ehi_name :: Var          -- ^ Name of the variable
  , ExampleHyInfo -> ExampleType
ehi_type :: ExampleType  -- ^ Type of the variable
  }


------------------------------------------------------------------------------
-- | A variable
newtype Var = Var
  { Var -> Text
getVar :: Text
  }
  deriving newtype (String -> Var
(String -> Var) -> IsString Var
forall a. (String -> a) -> IsString a
fromString :: String -> Var
$cfromString :: String -> Var
IsString, [Var] -> Doc ann
Var -> Doc ann
(forall ann. Var -> Doc ann)
-> (forall ann. [Var] -> Doc ann) -> Pretty Var
forall ann. [Var] -> Doc ann
forall ann. Var -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
prettyList :: [Var] -> Doc ann
$cprettyList :: forall ann. [Var] -> Doc ann
pretty :: Var -> Doc ann
$cpretty :: forall ann. Var -> Doc ann
Pretty)


------------------------------------------------------------------------------
-- | A type
newtype ExampleType = ExampleType
  { ExampleType -> Text
getExampleType :: Text
  }
  deriving newtype (String -> ExampleType
(String -> ExampleType) -> IsString ExampleType
forall a. (String -> a) -> IsString a
fromString :: String -> ExampleType
$cfromString :: String -> ExampleType
IsString, [ExampleType] -> Doc ann
ExampleType -> Doc ann
(forall ann. ExampleType -> Doc ann)
-> (forall ann. [ExampleType] -> Doc ann) -> Pretty ExampleType
forall ann. [ExampleType] -> Doc ann
forall ann. ExampleType -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
prettyList :: [ExampleType] -> Doc ann
$cprettyList :: forall ann. [ExampleType] -> Doc ann
pretty :: ExampleType -> Doc ann
$cpretty :: forall ann. ExampleType -> Doc ann
Pretty)


------------------------------------------------------------------------------
-- | A command to expose to the parser
data MetaprogramCommand a = MC
  { MetaprogramCommand a -> Text
mpc_name        :: Text         -- ^ Name of the command. This is the token necessary to run the command.
  , MetaprogramCommand a -> Syntax a
mpc_syntax      :: Syntax a     -- ^ The command's arguments
  , MetaprogramCommand a -> Determinism
mpc_det         :: Determinism  -- ^ Determinism of the command
  , MetaprogramCommand a -> Text
mpc_description :: Text         -- ^ User-facing description
  , MetaprogramCommand a -> a
mpc_tactic      :: a            -- ^ Tactic to run
  , MetaprogramCommand a -> [Example]
mpc_examples    :: [Example]    -- ^ Collection of documentation examples
  }

------------------------------------------------------------------------------
-- | Existentialize the pain away
data SomeMetaprogramCommand where
  SMC :: MetaprogramCommand a -> SomeMetaprogramCommand


------------------------------------------------------------------------------
-- | Run the 'Parser' of a 'MetaprogramCommand'
makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())
makeMPParser :: MetaprogramCommand a -> Parser (TacticsM ())
makeMPParser (MC Text
name Syntax a
Nullary Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  a
Parser (TacticsM ())
t
makeMPParser (MC Text
name (Ref Count a
One) Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  Parser OccName
variable Parser OccName
-> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a
OccName -> Parser (TacticsM ())
t
makeMPParser (MC Text
name (Ref Count a
Many) Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  Parser OccName -> ParsecT Void Text Identity [OccName]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many Parser OccName
variable ParsecT Void Text Identity [OccName]
-> ([OccName] -> Parser (TacticsM ())) -> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a
[OccName] -> Parser (TacticsM ())
t
makeMPParser (MC Text
name (Bind Count a
One) Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  Parser OccName
variable Parser OccName
-> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a
OccName -> Parser (TacticsM ())
t
makeMPParser (MC Text
name (Bind Count a
Many) Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  Parser OccName -> ParsecT Void Text Identity [OccName]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many Parser OccName
variable ParsecT Void Text Identity [OccName]
-> ([OccName] -> Parser (TacticsM ())) -> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a
[OccName] -> Parser (TacticsM ())
t
makeMPParser (MC Text
name Syntax a
Tactic Determinism
_ Text
_ a
t [Example]
_) = do
  Text -> Parser ()
identifier Text
name
  Parser (TacticsM ()) -> Parser (TacticsM ())
forall a. Parser a -> Parser a
parens Parser (TacticsM ())
tactic Parser (TacticsM ())
-> (TacticsM () -> Parser (TacticsM ())) -> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a
TacticsM () -> Parser (TacticsM ())
t


------------------------------------------------------------------------------
-- | Compile a collection of metaprogram commands into a parser.
makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())
makeParser :: [SomeMetaprogramCommand] -> Parser (TacticsM ())
makeParser [SomeMetaprogramCommand]
ps = [Parser (TacticsM ())] -> Parser (TacticsM ())
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice ([Parser (TacticsM ())] -> Parser (TacticsM ()))
-> [Parser (TacticsM ())] -> Parser (TacticsM ())
forall a b. (a -> b) -> a -> b
$ [SomeMetaprogramCommand]
ps [SomeMetaprogramCommand]
-> (SomeMetaprogramCommand -> Parser (TacticsM ()))
-> [Parser (TacticsM ())]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(SMC MetaprogramCommand a
mp) -> MetaprogramCommand a -> Parser (TacticsM ())
forall a. MetaprogramCommand a -> Parser (TacticsM ())
makeMPParser MetaprogramCommand a
mp


------------------------------------------------------------------------------
-- | Pretty print a command.
prettyCommand :: MetaprogramCommand a -> Doc b
prettyCommand :: MetaprogramCommand a -> Doc b
prettyCommand (MC Text
name Syntax a
syn Determinism
det Text
desc a
_ [Example]
exs) = [Doc b] -> Doc b
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc b
"##" Doc b -> Doc b -> Doc b
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc b
forall a ann. Pretty a => a -> Doc ann
pretty Text
name
  , Doc b
forall a. Monoid a => a
mempty
  , Doc b
"arguments:" Doc b -> Doc b -> Doc b
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Syntax a -> Doc b
forall a b. Syntax a -> Doc b
prettySyntax Syntax a
syn Doc b -> Doc b -> Doc b
forall a. Semigroup a => a -> a -> a
<> Doc b
".  "
  , Determinism -> Doc b
forall b. Determinism -> Doc b
prettyDeterminism Determinism
det Doc b -> Doc b -> Doc b
forall a. Semigroup a => a -> a -> a
<> Doc b
"."
  , Doc b
forall a. Monoid a => a
mempty
  , Doc b
">" Doc b -> Doc b -> Doc b
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc b -> Doc b
forall ann. Doc ann -> Doc ann
align (Text -> Doc b
forall a ann. Pretty a => a -> Doc ann
pretty Text
desc)
  , Doc b
forall a. Monoid a => a
mempty
  , [Doc b] -> Doc b
forall ann. [Doc ann] -> Doc ann
vsep ([Doc b] -> Doc b) -> [Doc b] -> Doc b
forall a b. (a -> b) -> a -> b
$ (Example -> Doc b) -> [Example] -> [Doc b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Example -> Doc b
forall a. Text -> Example -> Doc a
prettyExample Text
name) [Example]
exs
  , Doc b
forall a. Monoid a => a
mempty
  ]


------------------------------------------------------------------------------
-- | Pretty print a hypothesis.
prettyHyInfo :: ExampleHyInfo -> Doc a
prettyHyInfo :: ExampleHyInfo -> Doc a
prettyHyInfo ExampleHyInfo
hi = Var -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty (ExampleHyInfo -> Var
ehi_name ExampleHyInfo
hi) Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a
"::" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ExampleType -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty (ExampleHyInfo -> ExampleType
ehi_type ExampleHyInfo
hi)


------------------------------------------------------------------------------
-- | Append the given term only if the first argument has elements.
mappendIfNotNull :: [a] -> a -> [a]
mappendIfNotNull :: [a] -> a -> [a]
mappendIfNotNull [] a
_ = []
mappendIfNotNull [a]
as a
a = [a]
as [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a
a]


------------------------------------------------------------------------------
-- | Pretty print an example.
prettyExample :: Text -> Example -> Doc a
prettyExample :: Text -> Example -> Doc a
prettyExample Text
name (Example Maybe Text
m_txt [Var]
args [ExampleHyInfo]
hys Maybe ExampleType
goal Text
res) =
  Doc a -> Doc a
forall ann. Doc ann -> Doc ann
align (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc a
forall a. Monoid a => a
mempty
    , Doc a
"### Example"
    , Doc a -> (Text -> Doc a) -> Maybe Text -> Doc a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc a
forall a. Monoid a => a
mempty ((Doc a
forall ann. Doc ann
line Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<>) (Doc a -> Doc a) -> (Text -> Doc a) -> Text -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> Doc a
forall ann. Doc ann
line) (Doc a -> Doc a) -> (Text -> Doc a) -> Text -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc a
">" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc a -> Doc a) -> (Text -> Doc a) -> Text -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc a -> Doc a
forall ann. Doc ann -> Doc ann
align (Doc a -> Doc a) -> (Text -> Doc a) -> Text -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty) Maybe Text
m_txt
    , Doc a
"Given:"
    , Doc a
forall a. Monoid a => a
mempty
    , Doc a -> Doc a
forall ann. Doc ann -> Doc ann
codeFence (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep
        ([Doc a] -> Doc a) -> [Doc a] -> Doc a
forall a b. (a -> b) -> a -> b
$ [Doc a] -> Doc a -> [Doc a]
forall a. [a] -> a -> [a]
mappendIfNotNull ((ExampleHyInfo -> Doc a) -> [ExampleHyInfo] -> [Doc a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExampleHyInfo -> Doc a
forall a. ExampleHyInfo -> Doc a
prettyHyInfo [ExampleHyInfo]
hys) Doc a
forall a. Monoid a => a
mempty
           [Doc a] -> [Doc a] -> [Doc a]
forall a. Semigroup a => a -> a -> a
<> [ Doc a
"_" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc a -> (ExampleType -> Doc a) -> Maybe ExampleType -> Doc a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc a
forall a. Monoid a => a
mempty ((Doc a
"::" Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann
<+>)(Doc a -> Doc a) -> (ExampleType -> Doc a) -> ExampleType -> Doc a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExampleType -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty) Maybe ExampleType
goal
              ]
    , Doc a
forall a. Monoid a => a
mempty
    , [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
hsep
        [ Doc a
"running "
        , Doc a -> Doc a -> Doc a -> Doc a
forall ann. Doc ann -> Doc ann -> Doc ann -> Doc ann
enclose Doc a
"`" Doc a
"`" (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
name Doc a -> Doc a -> Doc a
forall a. Semigroup a => a -> a -> a
<> [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
hsep (Doc a
forall a. Monoid a => a
mempty Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: (Var -> Doc a) -> [Var] -> [Doc a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty [Var]
args)
        , Doc a
"will produce:"
        ]
    , Doc a
forall a. Monoid a => a
mempty
    , Doc a -> Doc a
forall ann. Doc ann -> Doc ann
codeFence (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ Doc a -> Doc a
forall ann. Doc ann -> Doc ann
align (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ Text -> Doc a
forall a ann. Pretty a => a -> Doc ann
pretty Text
res
    ]


------------------------------------------------------------------------------
-- | Make a haskell code fence.
codeFence :: Doc a -> Doc a
codeFence :: Doc a -> Doc a
codeFence Doc a
d = Doc a -> Doc a
forall ann. Doc ann -> Doc ann
align (Doc a -> Doc a) -> Doc a -> Doc a
forall a b. (a -> b) -> a -> b
$ [Doc a] -> Doc a
forall ann. [Doc ann] -> Doc ann
vsep
  [ Doc a
"```haskell"
  , Doc a
d
  , Doc a
"```"
  ]


------------------------------------------------------------------------------
-- | Render all of the commands.
prettyReadme :: [SomeMetaprogramCommand] -> String
prettyReadme :: [SomeMetaprogramCommand] -> String
prettyReadme
  = SimpleDocStream Any -> String
forall ann. SimpleDocStream ann -> String
renderString
  (SimpleDocStream Any -> String)
-> ([SomeMetaprogramCommand] -> SimpleDocStream Any)
-> [SomeMetaprogramCommand]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Any -> SimpleDocStream Any
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions
  (Doc Any -> SimpleDocStream Any)
-> ([SomeMetaprogramCommand] -> Doc Any)
-> [SomeMetaprogramCommand]
-> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc Any] -> Doc Any
forall ann. [Doc ann] -> Doc ann
vsep
  ([Doc Any] -> Doc Any)
-> ([SomeMetaprogramCommand] -> [Doc Any])
-> [SomeMetaprogramCommand]
-> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeMetaprogramCommand -> Doc Any)
-> [SomeMetaprogramCommand] -> [Doc Any]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case SMC MetaprogramCommand a
c -> MetaprogramCommand a -> Doc Any
forall a b. MetaprogramCommand a -> Doc b
prettyCommand MetaprogramCommand a
c)
  ([SomeMetaprogramCommand] -> [Doc Any])
-> ([SomeMetaprogramCommand] -> [SomeMetaprogramCommand])
-> [SomeMetaprogramCommand]
-> [Doc Any]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeMetaprogramCommand -> Text)
-> [SomeMetaprogramCommand] -> [SomeMetaprogramCommand]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\case SMC MetaprogramCommand a
c -> MetaprogramCommand a -> Text
forall a. MetaprogramCommand a -> Text
mpc_name MetaprogramCommand a
c)



------------------------------------------------------------------------------
-- | Helper function to build a 'SomeMetaprogramCommand'.
command
    :: Text
    -> Determinism
    -> Syntax a
    -> Text
    -> a
    -> [Example]
    -> SomeMetaprogramCommand
command :: Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
txt Determinism
det Syntax a
syn Text
txt' a
a [Example]
exs = MetaprogramCommand a -> SomeMetaprogramCommand
forall a. MetaprogramCommand a -> SomeMetaprogramCommand
SMC (MetaprogramCommand a -> SomeMetaprogramCommand)
-> MetaprogramCommand a -> SomeMetaprogramCommand
forall a b. (a -> b) -> a -> b
$
  MC :: forall a.
Text
-> Syntax a
-> Determinism
-> Text
-> a
-> [Example]
-> MetaprogramCommand a
MC
    { mpc_name :: Text
mpc_name        = Text
txt
    , mpc_det :: Determinism
mpc_det         = Determinism
det
    , mpc_syntax :: Syntax a
mpc_syntax      = Syntax a
syn
    , mpc_description :: Text
mpc_description = Text
txt'
    , mpc_tactic :: a
mpc_tactic      = a
a
    , mpc_examples :: [Example]
mpc_examples    = [Example]
exs
    }