@@ -8,16 +8,15 @@ module Wingman.Metaprogramming.Parser where
88
99import qualified Control.Monad.Combinators.Expr as P
1010import 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 )
1313import qualified Refinery.Tactic as R
1414import qualified Text.Megaparsec as P
1515import Wingman.Auto
1616import Wingman.LanguageServer.TacticProviders (useNameFromHypothesis )
1717import Wingman.Metaprogramming.Lexer
1818import Wingman.Tactics
1919import Wingman.Types
20- import qualified Data.Text as T
2120
2221
2322nullary :: T. Text -> TacticsM () -> Parser (TacticsM () )
@@ -62,22 +61,15 @@ bindOne t t1 = t R.<@> [t1]
6261
6362operators :: [[P. Operator Parser (TacticsM () )]]
6463operators =
65- [ [ P. Prefix (symbol " *" $> R. many_) ]
64+ [ [ P. Prefix (symbol " *" $> R. many_) ]
6665 , [ 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)
7069 ]
7170 ]
7271
7372
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-
8173attempt_it :: Context -> Judgement -> String -> Either String (LHsExpr GhcPs )
8274attempt_it ctx jdg program =
8375 case P. runParser (sc *> tactic <* P. eof) " <splice>" (T. pack program) of
0 commit comments