@@ -8,16 +8,15 @@ module Wingman.Metaprogramming.Parser where
8
8
9
9
import qualified Control.Monad.Combinators.Expr as P
10
10
import Data.Functor
11
- import Development.IDE.GHC.Compat ( alphaTyVars , LHsExpr , GhcPs )
12
- import GhcPlugins ( mkTyVarTy )
11
+ import qualified Data.Text as T
12
+ import Development.IDE.GHC.Compat ( LHsExpr , GhcPs )
13
13
import qualified Refinery.Tactic as R
14
14
import qualified Text.Megaparsec as P
15
15
import Wingman.Auto
16
16
import Wingman.LanguageServer.TacticProviders (useNameFromHypothesis )
17
17
import Wingman.Metaprogramming.Lexer
18
18
import Wingman.Tactics
19
19
import Wingman.Types
20
- import qualified Data.Text as T
21
20
22
21
23
22
nullary :: T. Text -> TacticsM () -> Parser (TacticsM () )
@@ -62,25 +61,18 @@ bindOne t t1 = t R.<@> [t1]
62
61
63
62
operators :: [[P. Operator Parser (TacticsM () )]]
64
63
operators =
65
- [ [ P. Prefix (symbol " *" $> R. many_) ]
64
+ [ [ P. Prefix (symbol " *" $> R. many_) ]
66
65
, [ P. Prefix (symbol " try" $> R. try) ]
67
- , [ P. InfixR (symbol " |" $> (R. <%>) )]
68
- , [ P. InfixL (symbol " ;" $> (>>) )
69
- , P. InfixL (symbol " ," $> bindOne)
66
+ , [ P. InfixR (symbol " |" $> (R. <%>) )]
67
+ , [ P. InfixL (symbol " ;" $> (>>) )
68
+ , P. InfixL (symbol " ," $> bindOne)
70
69
]
71
70
]
72
71
73
72
74
- skolems :: [Type ]
75
- skolems = fmap mkTyVarTy alphaTyVars
76
-
77
- a_skolem , b_skolem , c_skolem :: Type
78
- (a_skolem : b_skolem : c_skolem : _) = skolems
79
-
80
-
81
73
attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs )
82
74
attempt_it ctx jdg program =
83
- case P. runParser (sc *> tactic <* P. eof) " <splice>" ( T. pack program) of
75
+ case P. runParser (sc *> tactic <* P. eof) " <splice>" $ T. pack program of
84
76
Left peb -> Left $ P. errorBundlePretty peb
85
77
Right tt -> do
86
78
case runTactic
0 commit comments