{-# 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)
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_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>"
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
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
]