{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}

module Wingman.Metaprogramming.Parser where

import qualified Control.Monad.Combinators.Expr as P
import qualified Control.Monad.Error.Class as E
import           Control.Monad.Reader (ReaderT, ask, MonadIO (liftIO), asks)
import           Data.Functor
import           Data.Maybe (listToMaybe)
import qualified Data.Text as T
import           GhcPlugins (occNameString)
import qualified Refinery.Tactic as R
import qualified Text.Megaparsec as P
import           Wingman.Auto
import           Wingman.Context (getCurrentDefinitions)
import           Wingman.Machinery (useNameFromHypothesis, getOccNameType, createImportedHyInfo, useNameFromContext, lookupNameInContext)
import           Wingman.Metaprogramming.Lexer
import           Wingman.Metaprogramming.Parser.Documentation
import           Wingman.Metaprogramming.ProofState (proofState, layout)
import           Wingman.Tactics
import           Wingman.Types


nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
nullary :: Text -> TacticsM () -> Parser (TacticsM ())
nullary Text
name TacticsM ()
tac = Text -> Parser ()
identifier Text
name Parser () -> TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM ()
tac


unary_occ :: T.Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
unary_occ :: Text -> (OccName -> TacticsM ()) -> Parser (TacticsM ())
unary_occ Text
name OccName -> TacticsM ()
tac = OccName -> TacticsM ()
tac (OccName -> TacticsM ())
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
-> Parser (TacticsM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser ()
identifier Text
name Parser ()
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text (ReaderT ParserContext IO) OccName
variable)


------------------------------------------------------------------------------
-- | Like 'unary_occ', but runs directly in the 'Parser' monad.
unary_occM :: T.Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
unary_occM :: Text -> (OccName -> Parser (TacticsM ())) -> Parser (TacticsM ())
unary_occM Text
name OccName -> Parser (TacticsM ())
tac = OccName -> Parser (TacticsM ())
tac (OccName -> Parser (TacticsM ()))
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
-> Parser (TacticsM ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Text -> Parser ()
identifier Text
name Parser ()
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
-> ParsecT Void Text (ReaderT ParserContext IO) OccName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text (ReaderT ParserContext IO) OccName
variable)


variadic_occ :: T.Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
variadic_occ :: Text -> ([OccName] -> TacticsM ()) -> Parser (TacticsM ())
variadic_occ Text
name [OccName] -> TacticsM ()
tac = [OccName] -> TacticsM ()
tac ([OccName] -> TacticsM ())
-> ParsecT Void Text (ReaderT ParserContext IO) [OccName]
-> Parser (TacticsM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser ()
identifier Text
name Parser ()
-> ParsecT Void Text (ReaderT ParserContext IO) [OccName]
-> ParsecT Void Text (ReaderT ParserContext IO) [OccName]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text (ReaderT ParserContext IO) OccName
-> ParsecT Void Text (ReaderT ParserContext IO) [OccName]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ParsecT Void Text (ReaderT ParserContext IO) OccName
variable)


commands :: [SomeMetaprogramCommand]
commands :: [SomeMetaprogramCommand]
commands =
  [ Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"assumption" Determinism
Nondeterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Use any term in the hypothesis that can unify with the current goal."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
assumption)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"some_a_val" ExampleType
"a"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a")
          Text
"some_a_val"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"assume" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Use the given term from the hypothesis, unifying it with the current goal"
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> TacticsM ()
assume)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"some_a_val"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"some_a_val" ExampleType
"a"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a")
          Text
"some_a_val"
      ]

  , Text
-> Determinism
-> Syntax ([OccName] -> Parser (TacticsM ()))
-> Text
-> ([OccName] -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"intros" Determinism
Deterministic (Count [OccName] -> Syntax ([OccName] -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Bind Count [OccName]
Many)
      ( [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
          [ Text
"Construct a lambda expression, using the specific names if given, "
          , Text
"generating unique names otherwise. When no arguments are given, "
          , Text
"all of the function arguments will be bound; otherwise, this "
          , Text
"tactic will bind only enough to saturate the given names. Extra "
          , Text
"names are ignored."
          ])
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> ([OccName] -> TacticsM ()) -> [OccName] -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
        []    -> TacticsM ()
intros
        [OccName]
names -> Maybe [OccName] -> TacticsM ()
intros' (Maybe [OccName] -> TacticsM ()) -> Maybe [OccName] -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [OccName] -> Maybe [OccName]
forall a. a -> Maybe a
Just [OccName]
names
      )
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a -> b -> c -> d")
          Text
"\\a b c -> (_ :: d)"
      , Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"aye"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a -> b -> c -> d")
          Text
"\\aye -> (_ :: b -> c -> d)"
      , Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"x", Var
"y", Var
"z", Var
"w"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a -> b -> c -> d")
          Text
"\\x y z -> (_ :: d)"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"intro" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Bind Count OccName
One)
      Text
"Construct a lambda expression, binding an argument with the given name."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [OccName] -> TacticsM ()
intros' (Maybe [OccName] -> TacticsM ())
-> (OccName -> Maybe [OccName]) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccName] -> Maybe [OccName]
forall a. a -> Maybe a
Just ([OccName] -> Maybe [OccName])
-> (OccName -> [OccName]) -> OccName -> Maybe [OccName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> [OccName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"aye"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a -> b -> c -> d")
          Text
"\\aye -> (_ :: b -> c -> d)"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"destruct_all" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Pattern match on every function paramater, in original binding order."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
destructAll)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"Assume `a` and `b` were bound via `f a b = _`.")
          []
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"a" ExampleType
"Bool", Var -> ExampleType -> ExampleHyInfo
EHI Var
"b" ExampleType
"Maybe Int"]
          Maybe ExampleType
forall a. Maybe a
Nothing (Text -> Example) -> Text -> Example
forall a b. (a -> b) -> a -> b
$
          String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
            [ String
"case a of"
            , String
"  False -> case b of"
            , String
"    Nothing -> _"
            , String
"    Just i -> _"
            , String
"  True -> case b of"
            , String
"    Nothing -> _"
            , String
"    Just i -> _"
            ]
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"destruct" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Pattern match on the argument."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
destruct)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"a"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"a" ExampleType
"Bool"]
          Maybe ExampleType
forall a. Maybe a
Nothing (Text -> Example) -> Text -> Example
forall a b. (a -> b) -> a -> b
$
          String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
            [ String
"case a of"
            , String
"  False -> _"
            , String
"  True -> _"
            ]
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"homo" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      ( [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
        [ Text
"Pattern match on the argument, and fill the resulting hole in with "
        , Text
"the same data constructor."
        ])
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
homo)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
            [ Text
"Only applicable when the type constructor of the argument is "
            , Text
"the same as that of the hole."
            ])
          [Var
"e"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"e" ExampleType
"Either a b"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Either x y") (Text -> Example) -> Text -> Example
forall a b. (a -> b) -> a -> b
$
          String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
            [ String
"case e of"
            , String
"  Left a -> Left (_ :: x)"
            , String
"  Right b -> Right (_ :: y)"
            ]
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"application" Determinism
Nondeterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Apply any function in the hypothesis that returns the correct type."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
application)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"f" ExampleType
"a -> b"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"b")
          Text
"f (_ :: a)"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"apply" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Apply the given function from *local* scope."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
apply)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"f"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"f" ExampleType
"a -> b"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"b")
          Text
"f (_ :: a)"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"split" Determinism
Nondeterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Produce a data constructor for the current goal."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
split)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Either a b")
          Text
"Right (_ :: b)"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"ctor" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Use the given data cosntructor."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> TacticsM ()
userSplit)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"Just"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Maybe a")
          Text
"Just (_ :: a)"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"obvious" Determinism
Nondeterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Produce a nullary data constructor for the current goal."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
obvious)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"[a]")
          Text
"[]"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"auto" Determinism
Nondeterministic Syntax (Parser (TacticsM ()))
Nullary
      ( [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
          [ Text
"Repeatedly attempt to split, destruct, apply functions, and "
          , Text
"recurse in an attempt to fill the hole."
          ])
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
auto)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"f" ExampleType
"a -> b", Var -> ExampleType -> ExampleHyInfo
EHI Var
"g" ExampleType
"b -> c"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a -> c")
          Text
"g . f"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"sorry" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"\"Solve\" the goal by leaving a hole."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
sorry)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"b")
          Text
"_ :: b"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"unary" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      ( [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
        [ Text
"Produce a hole for a single-parameter function, as well as a hole for "
        , Text
"its argument. The argument holes are completely unconstrained, and "
        , Text
"will be solved before the function."
        ])
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> TacticsM () -> Parser (TacticsM ())
forall a b. (a -> b) -> a -> b
$ Int -> TacticsM ()
nary Int
1)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
            [ Text
"In the example below, the variable `a` is free, and will unify "
            , Text
"to the resulting extract from any subsequent tactic."
            ])
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Int")
          Text
"(_2 :: a -> Int) (_1 :: a)"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"binary" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      ( [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
        [ Text
"Produce a hole for a two-parameter function, as well as holes for "
        , Text
"its arguments. The argument holes have the same type but are "
        , Text
"otherwise unconstrained, and will be solved before the function."
        ])
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> TacticsM () -> Parser (TacticsM ())
forall a b. (a -> b) -> a -> b
$ Int -> TacticsM ()
nary Int
2)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat
            [ Text
"In the example below, the variable `a` is free, and will unify "
            , Text
"to the resulting extract from any subsequent tactic."
            ])
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Int")
          Text
"(_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"recursion" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Fill the current hole with a call to the defining function."
      ( TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> TacticsM () -> Parser (TacticsM ())
forall a b. (a -> b) -> a -> b
$
          ([(OccName, CType)] -> Maybe (OccName, CType))
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     [(OccName, CType)]
-> TacticT
     Judgement
     (Synthesized (LHsExpr GhcPs))
     TacticError
     TacticState
     ExtractM
     (Maybe (OccName, CType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(OccName, CType)] -> Maybe (OccName, CType)
forall a. [a] -> Maybe a
listToMaybe TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  [(OccName, CType)]
forall (m :: * -> *). MonadReader Context m => m [(OccName, CType)]
getCurrentDefinitions TacticT
  Judgement
  (Synthesized (LHsExpr GhcPs))
  TacticError
  TacticState
  ExtractM
  (Maybe (OccName, CType))
-> (Maybe (OccName, CType) -> TacticsM ()) -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just (OccName
self, CType
_) -> (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromContext HyInfo CType -> TacticsM ()
apply OccName
self
            Maybe (OccName, CType)
Nothing -> TacticError -> TacticsM ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
E.throwError (TacticError -> TacticsM ()) -> TacticError -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ String -> TacticError
TacticPanic String
"no defining function"
      )
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"In the context of `foo (a :: Int) (b :: b) = _`:")
          []
          []
          Maybe ExampleType
forall a. Maybe a
Nothing
          Text
"foo (_ :: Int) (_ :: b)"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"use" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Apply the given function from *module* scope."
      ( \OccName
occ -> do
          Context
ctx <- (ParserContext -> Context)
-> ParsecT Void Text (ReaderT ParserContext IO) Context
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ParserContext -> Context
ps_context
          CType
ty <- case OccName -> Context -> Maybe CType
forall (m :: * -> *).
MonadReader Context m =>
OccName -> m (Maybe CType)
lookupNameInContext OccName
occ Context
ctx of
            Just CType
ty -> CType -> ParsecT Void Text (ReaderT ParserContext IO) CType
forall (f :: * -> *) a. Applicative f => a -> f a
pure CType
ty
            Maybe CType
Nothing -> Type -> CType
CType (Type -> CType)
-> ParsecT Void Text (ReaderT ParserContext IO) Type
-> ParsecT Void Text (ReaderT ParserContext IO) CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OccName -> ParsecT Void Text (ReaderT ParserContext IO) Type
getOccTy OccName
occ
          TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> TacticsM () -> Parser (TacticsM ())
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> TacticsM ()
apply (HyInfo CType -> TacticsM ()) -> HyInfo CType -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ OccName -> CType -> HyInfo CType
createImportedHyInfo OccName
occ CType
ty
      )
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"`import Data.Char (isSpace)`")
          [Var
"isSpace"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Bool")
          Text
"isSpace (_ :: Char)"
      ]

  , Text
-> Determinism
-> Syntax (OccName -> Parser (TacticsM ()))
-> Text
-> (OccName -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"cata" Determinism
Deterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Destruct the given term, recursing on every resulting binding."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (OccName -> TacticsM ()) -> OccName -> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> TacticsM ()) -> OccName -> TacticsM ()
forall a. (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
useNameFromHypothesis HyInfo CType -> TacticsM ()
cata)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"Assume we're called in the context of a function `f.`")
          [Var
"x"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"x" ExampleType
"(a, a)"]
          Maybe ExampleType
forall a. Maybe a
Nothing (Text -> Example) -> Text -> Example
forall a b. (a -> b) -> a -> b
$
          String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
init (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
            [ String
"case x of"
            , String
"  (a1, a2) ->"
            , String
"    let a1_c = f a1"
            , String
"        a2_c = f a2"
            , String
"     in _"
            ]
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"collapse" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Collapse every term in scope with the same type as the goal."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
collapse)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          []
          [ Var -> ExampleType -> ExampleHyInfo
EHI Var
"a1" ExampleType
"a"
          , Var -> ExampleType -> ExampleHyInfo
EHI Var
"a2" ExampleType
"a"
          , Var -> ExampleType -> ExampleHyInfo
EHI Var
"a3" ExampleType
"a"
          ]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"a")
          Text
"(_ :: a -> a -> a -> a) a1 a2 a3"
      ]

  ]



oneTactic :: Parser (TacticsM ())
oneTactic :: Parser (TacticsM ())
oneTactic =
  [Parser (TacticsM ())] -> Parser (TacticsM ())
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice
    [ Parser (TacticsM ()) -> Parser (TacticsM ())
forall a. Parser a -> Parser a
parens Parser (TacticsM ())
tactic
    , [SomeMetaprogramCommand] -> Parser (TacticsM ())
makeParser [SomeMetaprogramCommand]
commands
    ]


tactic :: Parser (TacticsM ())
tactic :: Parser (TacticsM ())
tactic = (Parser (TacticsM ())
 -> [[Operator Parser (TacticsM ())]] -> Parser (TacticsM ()))
-> [[Operator Parser (TacticsM ())]]
-> Parser (TacticsM ())
-> Parser (TacticsM ())
forall a b c. (a -> b -> c) -> b -> a -> c
flip Parser (TacticsM ())
-> [[Operator Parser (TacticsM ())]] -> Parser (TacticsM ())
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
P.makeExprParser [[Operator Parser (TacticsM ())]]
operators Parser (TacticsM ())
oneTactic

bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne :: TacticsM a -> TacticsM a -> TacticsM a
bindOne TacticsM a
t TacticsM a
t1 = TacticsM a
t TacticsM a -> [TacticsM a] -> TacticsM a
forall (m :: * -> *) jdg ext err s a.
Functor m =>
TacticT jdg ext err s m a
-> [TacticT jdg ext err s m a] -> TacticT jdg ext err s m a
R.<@> [TacticsM a
t1]

operators :: [[P.Operator Parser (TacticsM ())]]
operators :: [[Operator Parser (TacticsM ())]]
operators =
    [ [ ParsecT
  Void Text (ReaderT ParserContext IO) (TacticsM () -> TacticsM ())
-> Operator Parser (TacticsM ())
forall (m :: * -> *) a. m (a -> a) -> Operator m a
P.Prefix (Text -> Parser Text
symbol Text
"*"   Parser Text
-> (TacticsM () -> TacticsM ())
-> ParsecT
     Void Text (ReaderT ParserContext IO) (TacticsM () -> TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
R.many_) ]
    , [ ParsecT
  Void Text (ReaderT ParserContext IO) (TacticsM () -> TacticsM ())
-> Operator Parser (TacticsM ())
forall (m :: * -> *) a. m (a -> a) -> Operator m a
P.Prefix (Text -> Parser Text
symbol Text
"try" Parser Text
-> (TacticsM () -> TacticsM ())
-> ParsecT
     Void Text (ReaderT ParserContext IO) (TacticsM () -> TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
R.try) ]
    , [ ParsecT
  Void
  Text
  (ReaderT ParserContext IO)
  (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator Parser (TacticsM ())
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixR (Text -> Parser Text
symbol Text
"|"   Parser Text
-> (TacticsM () -> TacticsM () -> TacticsM ())
-> ParsecT
     Void
     Text
     (ReaderT ParserContext IO)
     (TacticsM () -> TacticsM () -> TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM () -> TacticsM () -> TacticsM ()
forall jdg ext err s (m :: * -> *) a.
TacticT jdg ext err s m a
-> TacticT jdg ext err s m a -> TacticT jdg ext err s m a
(R.<%>) )]
    , [ ParsecT
  Void
  Text
  (ReaderT ParserContext IO)
  (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator Parser (TacticsM ())
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL (Text -> Parser Text
symbol Text
";"   Parser Text
-> (TacticsM () -> TacticsM () -> TacticsM ())
-> ParsecT
     Void
     Text
     (ReaderT ParserContext IO)
     (TacticsM () -> TacticsM () -> TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM () -> TacticsM () -> TacticsM ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>))
      , ParsecT
  Void
  Text
  (ReaderT ParserContext IO)
  (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator Parser (TacticsM ())
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
P.InfixL (Text -> Parser Text
symbol Text
","   Parser Text
-> (TacticsM () -> TacticsM () -> TacticsM ())
-> ParsecT
     Void
     Text
     (ReaderT ParserContext IO)
     (TacticsM () -> TacticsM () -> TacticsM ())
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> TacticsM () -> TacticsM () -> TacticsM ()
forall a. TacticsM a -> TacticsM a -> TacticsM a
bindOne)
      ]
    ]


tacticProgram :: Parser (TacticsM ())
tacticProgram :: Parser (TacticsM ())
tacticProgram = do
  Parser ()
sc
  TacticsM ()
r <- Parser (TacticsM ())
tactic Parser (TacticsM ())
-> Parser (TacticsM ()) -> Parser (TacticsM ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
P.<|> TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
  TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
r


wrapError :: String -> String
wrapError :: String -> String
wrapError String
err = String
"```\n" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
err String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\n```\n"


------------------------------------------------------------------------------
-- | Attempt to run a metaprogram tactic, returning the proof state, or the
-- errors.
attempt_it
    :: Context
    -> Judgement
    -> String
    -> ReaderT ParserContext IO (Either String String)
attempt_it :: Context
-> Judgement
-> String
-> ReaderT ParserContext IO (Either String String)
attempt_it Context
ctx Judgement
jdg String
program =
  Parser (TacticsM ())
-> String
-> Text
-> ReaderT
     ParserContext
     IO
     (Either (ParseErrorBundle Text Void) (TacticsM ()))
forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> String -> s -> m (Either (ParseErrorBundle s e) a)
P.runParserT Parser (TacticsM ())
tacticProgram String
"<splice>" (String -> Text
T.pack String
program) ReaderT
  ParserContext
  IO
  (Either (ParseErrorBundle Text Void) (TacticsM ()))
-> (Either (ParseErrorBundle Text Void) (TacticsM ())
    -> Either String String)
-> ReaderT ParserContext IO (Either String String)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      Left ParseErrorBundle Text Void
peb -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ String -> String
wrapError (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle Text Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
P.errorBundlePretty ParseErrorBundle Text Void
peb
      Right TacticsM ()
tt -> do
        case Context
-> Judgement
-> TacticsM ()
-> Either [TacticError] RunTacticResults
runTactic
              Context
ctx
              Judgement
jdg
              TacticsM ()
tt
          of
            Left [TacticError]
tes -> String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ String -> String
wrapError (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [TacticError] -> String
forall a. Show a => a -> String
show [TacticError]
tes
            Right RunTacticResults
rtr -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Doc Ann -> String
layout (Doc Ann -> String) -> Doc Ann -> String
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> Doc Ann
proofState RunTacticResults
rtr


parseMetaprogram :: T.Text -> ReaderT ParserContext IO (TacticsM ())
parseMetaprogram :: Text -> ReaderT ParserContext IO (TacticsM ())
parseMetaprogram
    = (Either (ParseErrorBundle Text Void) (TacticsM ()) -> TacticsM ())
-> ReaderT
     ParserContext
     IO
     (Either (ParseErrorBundle Text Void) (TacticsM ()))
-> ReaderT ParserContext IO (TacticsM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ParseErrorBundle Text Void -> TacticsM ())
-> (TacticsM () -> TacticsM ())
-> Either (ParseErrorBundle Text Void) (TacticsM ())
-> TacticsM ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (TacticsM () -> ParseErrorBundle Text Void -> TacticsM ()
forall a b. a -> b -> a
const (TacticsM () -> ParseErrorBundle Text Void -> TacticsM ())
-> TacticsM () -> ParseErrorBundle Text Void -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ () -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) TacticsM () -> TacticsM ()
forall a. a -> a
id)
    (ReaderT
   ParserContext
   IO
   (Either (ParseErrorBundle Text Void) (TacticsM ()))
 -> ReaderT ParserContext IO (TacticsM ()))
-> (Text
    -> ReaderT
         ParserContext
         IO
         (Either (ParseErrorBundle Text Void) (TacticsM ())))
-> Text
-> ReaderT ParserContext IO (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser (TacticsM ())
-> String
-> Text
-> ReaderT
     ParserContext
     IO
     (Either (ParseErrorBundle Text Void) (TacticsM ()))
forall (m :: * -> *) e s a.
Monad m =>
ParsecT e s m a
-> String -> s -> m (Either (ParseErrorBundle s e) a)
P.runParserT Parser (TacticsM ())
tacticProgram String
"<splice>"


------------------------------------------------------------------------------
-- | Like 'getOccNameType', but runs in the 'Parser' monad.
getOccTy :: OccName -> Parser Type
getOccTy :: OccName -> ParsecT Void Text (ReaderT ParserContext IO) Type
getOccTy OccName
occ = do
  ParserContext HscEnv
hscenv OccEnv [GlobalRdrElt]
rdrenv Module
modul Context
_ <- ParsecT Void Text (ReaderT ParserContext IO) ParserContext
forall r (m :: * -> *). MonadReader r m => m r
ask
  Maybe Type
mty <- IO (Maybe Type)
-> ParsecT Void Text (ReaderT ParserContext IO) (Maybe Type)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Type)
 -> ParsecT Void Text (ReaderT ParserContext IO) (Maybe Type))
-> IO (Maybe Type)
-> ParsecT Void Text (ReaderT ParserContext IO) (Maybe Type)
forall a b. (a -> b) -> a -> b
$ HscEnv
-> OccEnv [GlobalRdrElt] -> Module -> OccName -> IO (Maybe Type)
getOccNameType HscEnv
hscenv OccEnv [GlobalRdrElt]
rdrenv Module
modul OccName
occ
  ParsecT Void Text (ReaderT ParserContext IO) Type
-> (Type -> ParsecT Void Text (ReaderT ParserContext IO) Type)
-> Maybe Type
-> ParsecT Void Text (ReaderT ParserContext IO) Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> ParsecT Void Text (ReaderT ParserContext IO) Type
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> ParsecT Void Text (ReaderT ParserContext IO) Type)
-> String -> ParsecT Void Text (ReaderT ParserContext IO) Type
forall a b. (a -> b) -> a -> b
$ OccName -> String
occNameString OccName
occ String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" is not in scope") Type -> ParsecT Void Text (ReaderT ParserContext IO) Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
mty


------------------------------------------------------------------------------
-- | Automatically generate the metaprogram command reference.
writeDocumentation :: IO ()
writeDocumentation :: IO ()
writeDocumentation =
  String -> String -> IO ()
writeFile String
"plugins/hls-tactics-plugin/COMMANDS.md" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
    [String] -> String
unlines
      [ String
"# Wingman Metaprogram Command Reference"
      , String
""
      , [SomeMetaprogramCommand] -> String
prettyReadme [SomeMetaprogramCommand]
commands
      ]