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

module Wingman.Metaprogramming.Parser where

import qualified Control.Monad.Combinators.Expr as P
import           Data.Either (fromRight)
import           Data.Functor
import           Data.Maybe (listToMaybe)
import qualified Data.Text as T
import           Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
import           Development.IDE.GHC.Compat.Util (unpackFS)
import           Refinery.Tactic (failure)
import qualified Refinery.Tactic as R
import qualified Text.Megaparsec as P
import           Wingman.Auto
import           Wingman.Machinery (useNameFromHypothesis, useNameFromContext, getCurrentDefinitions)
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 Identity OccName -> Parser (TacticsM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser ()
identifier Text
name Parser ()
-> ParsecT Void Text Identity OccName
-> ParsecT Void Text Identity OccName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity 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 Identity 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 Identity OccName
-> ParsecT Void Text Identity OccName
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity 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 Identity [OccName] -> Parser (TacticsM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser ()
identifier Text
name Parser ()
-> ParsecT Void Text Identity [OccName]
-> ParsecT Void Text Identity [OccName]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity OccName
-> ParsecT Void Text Identity [OccName]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ParsecT Void Text Identity 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 -> IntroParams -> TacticsM ()
intros' (IntroParams -> TacticsM ()) -> IntroParams -> TacticsM ()
forall a b. (a -> b) -> a -> b
$ [OccName] -> IntroParams
IntroduceOnlyNamed [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 (TacticsM () -> Parser (TacticsM ()))
-> Text
-> (TacticsM () -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"idiom" Determinism
Deterministic Syntax (TacticsM () -> Parser (TacticsM ()))
Tactic
      Text
"Lift a tactic into idiom brackets."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (TacticsM () -> TacticsM ())
-> TacticsM ()
-> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> TacticsM ()
idiom)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"(apply f)"]
          [Var -> ExampleType -> ExampleHyInfo
EHI Var
"f" ExampleType
"a -> b -> Int"]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"Maybe Int")
          Text
"f <$> (_ :: Maybe a) <*> (_ :: Maybe 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
"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
. IntroParams -> TacticsM ()
intros' (IntroParams -> TacticsM ())
-> (OccName -> IntroParams) -> OccName -> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OccName] -> IntroParams
IntroduceOnlyNamed ([OccName] -> IntroParams)
-> (OccName -> [OccName]) -> OccName -> IntroParams
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 (TacticsM () -> Parser (TacticsM ()))
-> Text
-> (TacticsM () -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"pointwise" Determinism
Deterministic Syntax (TacticsM () -> Parser (TacticsM ()))
Tactic
      Text
"Restrict the hypothesis in the holes of the given tactic to align up with the top-level bindings. This will ensure, eg, that the first hole can see only terms that came from the first position in any terms destructed from the top-level bindings."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (TacticsM () -> TacticsM ())
-> TacticsM ()
-> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TacticsM () -> TacticsM () -> TacticsM ())
-> TacticsM () -> TacticsM () -> TacticsM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip TacticsM () -> TacticsM () -> TacticsM ()
restrictPositionForApplication (() -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"In the context of `f (a1, b1) (a2, b2) = _`. The resulting first hole can see only 'a1' and 'a2', and the second, only 'b1' and 'b2'.")
          [Var
"(use mappend)"]
          []
          Maybe ExampleType
forall a. Maybe a
Nothing
          Text
"mappend _ _"
      ]

  , 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 (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated))
      [ 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)]
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 (Saturation -> HyInfo CType -> TacticsM ()
apply Saturation
Saturated) OccName
self
            Maybe (OccName, CType)
Nothing -> TacticError -> TacticsM ()
forall err jdg ext s (m :: * -> *) a.
err -> TacticT jdg ext err s m a
failure (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."
      (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
. Saturation -> OccName -> TacticsM ()
use Saturation
Saturated)
      [ 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"
      ]

  , Text
-> Determinism
-> Syntax ([OccName] -> Parser (TacticsM ()))
-> Text
-> ([OccName] -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"let" Determinism
Deterministic (Count [OccName] -> Syntax ([OccName] -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Bind Count [OccName]
Many)
      Text
"Create let-bindings for each binder given to this tactic."
      (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 ()
letBind)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"a", Var
"b", Var
"c"]
          [ ]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"x")
          (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
unlines
            [ String
"let a = _1 :: a"
            , String
"    b = _2 :: b"
            , String
"    c = _3 :: c"
            , String
" in (_4 :: x)"
            ]
      ]

  , Text
-> Determinism
-> Syntax (TacticsM () -> Parser (TacticsM ()))
-> Text
-> (TacticsM () -> Parser (TacticsM ()))
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"try" Determinism
Nondeterministic Syntax (TacticsM () -> Parser (TacticsM ()))
Tactic
      Text
"Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TacticsM () -> Parser (TacticsM ()))
-> (TacticsM () -> TacticsM ())
-> TacticsM ()
-> Parser (TacticsM ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TacticsM () -> TacticsM ()
forall (m :: * -> *) jdg ext err s.
Monad m =>
TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
R.try)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"(apply f)"]
          [ Var -> ExampleType -> ExampleHyInfo
EHI Var
"f" ExampleType
"a -> b"
          ]
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"b")
          (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
unlines
            [ String
"-- BOTH of:\n"
            , String
"f (_ :: a)"
            , String
"\n-- and\n"
            , String
"_ :: 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
"nested" Determinism
Nondeterministic (Count OccName -> Syntax (OccName -> Parser (TacticsM ()))
forall a. Count a -> Syntax (a -> Parser (TacticsM ()))
Ref Count OccName
One)
      Text
"Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context."
      (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 ()
nested)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          Maybe Text
forall a. Maybe a
Nothing
          [Var
"fmap"]
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"[(Int, Either Bool a)] -> [(Int, Either Bool b)]")
          Text
"fmap (fmap (fmap _))"
      ]

  , Text
-> Determinism
-> Syntax (Parser (TacticsM ()))
-> Text
-> Parser (TacticsM ())
-> [Example]
-> SomeMetaprogramCommand
forall a.
Text
-> Determinism
-> Syntax a
-> Text
-> a
-> [Example]
-> SomeMetaprogramCommand
command Text
"with_arg" Determinism
Deterministic Syntax (Parser (TacticsM ()))
Nullary
      Text
"Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context."
      (TacticsM () -> Parser (TacticsM ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure TacticsM ()
with_arg)
      [ Maybe Text
-> [Var] -> [ExampleHyInfo] -> Maybe ExampleType -> Text -> Example
Example
          (Text -> Maybe Text
forall a. a -> Maybe a
Just Text
"Where `a` is a new unifiable type variable.")
          []
          []
          (ExampleType -> Maybe ExampleType
forall a. a -> Maybe a
Just ExampleType
"r")
          Text
"(_2 :: a -> r) (_1 :: a)"
      ]
  ]



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 (ParsecT Void Text Identity) (TacticsM ())]]
-> Parser (TacticsM ())
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
P.makeExprParser Parser (TacticsM ())
oneTactic [[Operator (ParsecT Void Text Identity) (TacticsM ())]]
operators

operators :: [[P.Operator Parser (TacticsM ())]]
operators :: [[Operator (ParsecT Void Text Identity) (TacticsM ())]]
operators =
    [ [ ParsecT
  Void Text Identity (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator (ParsecT Void Text Identity) (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 Identity (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 Identity (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator (ParsecT Void Text Identity) (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 Identity (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 Identity (TacticsM () -> TacticsM () -> TacticsM ())
-> Operator (ParsecT Void Text Identity) (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 Identity (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"


fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b
fixErrorOffset :: RealSrcLoc -> ParseErrorBundle a b -> ParseErrorBundle a b
fixErrorOffset RealSrcLoc
rsl (P.ParseErrorBundle NonEmpty (ParseError a b)
ne (P.PosState a
a Int
n (P.SourcePos String
_ Pos
line Pos
col) Pos
pos String
s))
  = NonEmpty (ParseError a b) -> PosState a -> ParseErrorBundle a b
forall s e.
NonEmpty (ParseError s e) -> PosState s -> ParseErrorBundle s e
P.ParseErrorBundle NonEmpty (ParseError a b)
ne
  (PosState a -> ParseErrorBundle a b)
-> PosState a -> ParseErrorBundle a b
forall a b. (a -> b) -> a -> b
$ a -> Int -> SourcePos -> Pos -> String -> PosState a
forall s. s -> Int -> SourcePos -> Pos -> String -> PosState s
P.PosState a
a Int
n
      (String -> Pos -> Pos -> SourcePos
P.SourcePos
        (FastString -> String
unpackFS (FastString -> String) -> FastString -> String
forall a b. (a -> b) -> a -> b
$ RealSrcLoc -> FastString
srcLocFile RealSrcLoc
rsl)
        (Pos -> Pos -> Pos
forall a. Semigroup a => a -> a -> a
(<>) Pos
line (Pos -> Pos) -> Pos -> Pos
forall a b. (a -> b) -> a -> b
$ Int -> Pos
P.mkPos (Int -> Pos) -> Int -> Pos
forall a b. (a -> b) -> a -> b
$ RealSrcLoc -> Int
srcLocLine RealSrcLoc
rsl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        (Pos -> Pos -> Pos
forall a. Semigroup a => a -> a -> a
(<>) Pos
col  (Pos -> Pos) -> Pos -> Pos
forall a b. (a -> b) -> a -> b
$ Int -> Pos
P.mkPos (Int -> Pos) -> Int -> Pos
forall a b. (a -> b) -> a -> b
$ RealSrcLoc -> Int
srcLocCol  RealSrcLoc
rsl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length @[] String
"[wingman|")
      )
      Pos
pos
      String
s

------------------------------------------------------------------------------
-- | Attempt to run a metaprogram tactic, returning the proof state, or the
-- errors.
attempt_it
    :: RealSrcLoc
    -> Context
    -> Judgement
    -> String
    -> IO (Either String String)
attempt_it :: RealSrcLoc
-> Context -> Judgement -> String -> IO (Either String String)
attempt_it RealSrcLoc
rsl Context
ctx Judgement
jdg String
program =
  case Parser (TacticsM ())
-> String
-> Text
-> Either (ParseErrorBundle Text Void) (TacticsM ())
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
P.runParser Parser (TacticsM ())
tacticProgram String
"<splice>" (String -> Text
T.pack String
program) of
    Left ParseErrorBundle Text Void
peb -> Either String String -> IO (Either String String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String String -> IO (Either String String))
-> Either String String -> IO (Either String String)
forall a b. (a -> b) -> a -> b
$ 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 -> String)
-> ParseErrorBundle Text Void -> String
forall a b. (a -> b) -> a -> b
$ RealSrcLoc
-> ParseErrorBundle Text Void -> ParseErrorBundle Text Void
forall a b.
RealSrcLoc -> ParseErrorBundle a b -> ParseErrorBundle a b
fixErrorOffset RealSrcLoc
rsl ParseErrorBundle Text Void
peb
    Right TacticsM ()
tt -> do
      Either [TacticError] RunTacticResults
res <- Int
-> Context
-> Judgement
-> TacticsM ()
-> IO (Either [TacticError] RunTacticResults)
runTactic Int
2e6 Context
ctx Judgement
jdg TacticsM ()
tt
      Either String String -> IO (Either String String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String String -> IO (Either String String))
-> Either String String -> IO (Either String String)
forall a b. (a -> b) -> a -> b
$ case Either [TacticError] RunTacticResults
res 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
$ Bool -> Doc Ann -> String
layout (Config -> Bool
cfg_proofstate_styling (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Context -> Config
ctxConfig Context
ctx)
                     (Doc Ann -> String) -> Doc Ann -> String
forall a b. (a -> b) -> a -> b
$ RunTacticResults -> Doc Ann
proofState RunTacticResults
rtr


parseMetaprogram :: T.Text -> TacticsM ()
parseMetaprogram :: Text -> TacticsM ()
parseMetaprogram
    = TacticsM ()
-> Either (ParseErrorBundle Text Void) (TacticsM ()) -> TacticsM ()
forall b a. b -> Either a b -> b
fromRight (() -> TacticsM ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    (Either (ParseErrorBundle Text Void) (TacticsM ()) -> TacticsM ())
-> (Text -> Either (ParseErrorBundle Text Void) (TacticsM ()))
-> Text
-> TacticsM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser (TacticsM ())
-> String
-> Text
-> Either (ParseErrorBundle Text Void) (TacticsM ())
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
P.runParser Parser (TacticsM ())
tacticProgram String
"<splice>"


------------------------------------------------------------------------------
-- | Automatically generate the metaprogram command reference.
writeDocumentation :: IO ()
writeDocumentation :: IO ()
writeDocumentation =
  String -> String -> IO ()
writeFile String
"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
      ]