Upgrade to refinery-0.4.0.0

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

@@ -87,7 +87,7 @@ library
  , mtl
  , parser-combinators
  , prettyprinter
- , refinery ^>=0.3
+ , refinery ^>=0.4
  , retrie >=0.1.1.0
  , syb
  , text

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

@@ -59,7 +59,7 @@ destructMatches use_field_puns f scrut t jdg = do
  let hy = jEntireHypothesis jdg
  g = jGoal jdg
  case tacticsGetDataCons $ unCType t of
- Nothing -> throwError $ GoalMismatch "destruct" g
+ Nothing -> cut -- throwError $ GoalMismatch "destruct" g
  Just (dcs, apps) ->
  fmap unzipTrace $ for dcs $ \dc -> do
  let con = RealDataCon dc
@@ -214,7 +214,7 @@ patSynExTys ps = patSynExTyVars ps
 
 destruct' :: Bool -> (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
 destruct' use_field_puns f hi jdg = do
- when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
+ when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
  let term = hi_name hi
  ext
  <- destructMatches
@@ -234,13 +234,13 @@ destruct' use_field_puns f hi jdg = do
 -- resulting matches.
 destructLambdaCase' :: Bool -> (ConLike -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' use_field_puns f jdg = do
- when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
+ when (isDestructBlacklisted jdg) $ cut -- throwError NoApplicableTactic
  let g = jGoal jdg
  case splitFunTy_maybe (unCType g) of
  Just (arg, _) | isAlgType arg ->
  fmap (fmap noLoc lambdaCase) <$>
  destructMatches use_field_puns f Nothing (CType arg) jdg
- _ -> throwError $ GoalMismatch "destructLambdaCase'" g
+ _ -> cut -- throwError $ GoalMismatch "destructLambdaCase'" g
 
 
 ------------------------------------------------------------------------------
@@ -267,7 +267,7 @@ buildDataCon should_blacklist jdg dc tyapps = do
  --
  -- Fortunately, this isn't an issue in practice, since 'PatSyn's are
  -- never in the hypothesis.
- throwError $ TacticPanic "Can't build Pattern constructors yet"
+ cut -- throwError $ TacticPanic "Can't build Pattern constructors yet"
  ext
  <- fmap unzipTrace
  $ traverse ( \(arg, n) ->

plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs

@@ -1,6 +1,5 @@
 module Wingman.KnownStrategies where
 
-import Control.Monad.Error.Class
 import Data.Foldable (for_)
 import OccName (mkVarOcc, mkClsOcc)
 import Refinery.Tactic
@@ -26,7 +25,7 @@ known name t = do
  getCurrentDefinitions >>= \case
  [(def, _)] | def == mkVarOcc name ->
  tracing ("known " <> name) t
- _ -> throwError NoApplicableTactic
+ _ -> failure NoApplicableTactic
 
 
 deriveFmap :: TacticsM ()

plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs

@@ -1,7 +1,6 @@
 module Wingman.KnownStrategies.QuickCheck where
 
 import ConLike (ConLike(RealDataCon))
-import Control.Monad.Except (MonadError (throwError))
 import Data.Bool (bool)
 import Data.Generics (everything, mkQ)
 import Data.List (partition)
@@ -15,7 +14,7 @@ import GHC.SourceGen.Expr (case', lambda, let')
 import GHC.SourceGen.Overloaded (App ((@@)), HasList (list))
 import GHC.SourceGen.Pat (conP)
 import OccName (HasOccName (occName), mkVarOcc, occNameString)
-import Refinery.Tactic (goal, rule)
+import Refinery.Tactic (goal, rule, failure)
 import TyCon (TyCon, tyConDataCons, tyConName)
 import Type (splitTyConApp_maybe)
 import Wingman.CodeGen
@@ -61,7 +60,7 @@ deriveArbitrary = do
  (list $ fmap genExpr big)
  terminal_expr
  ]
- _ -> throwError $ GoalMismatch "deriveArbitrary" ty
+ _ -> failure $ GoalMismatch "deriveArbitrary" ty
 
 
 ------------------------------------------------------------------------------

plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

@@ -5,13 +5,11 @@ module Wingman.Machinery where
 
 import Control.Applicative (empty)
 import Control.Lens ((<>~))
-import Control.Monad.Error.Class
 import Control.Monad.Reader
 import Control.Monad.State.Class (gets, modify, MonadState)
 import Control.Monad.State.Strict (StateT (..), execStateT)
 import Control.Monad.Trans.Maybe
 import Data.Coerce
-import Data.Either
 import Data.Foldable
 import Data.Functor ((<&>))
 import Data.Generics (everything, gcount, mkQ)
@@ -96,20 +94,20 @@ runTactic ctx jdg t = do
  res <- flip runReaderT ctx
  . unExtractM
  $ runTacticT t jdg tacticState
- pure $ case partitionEithers res of
- (errs, []) -> Left $ take 50 errs
- (_, fmap assoc23 -> solns) -> do
+ pure $ case res of
+ (Left errs) -> Left $ take 50 errs
+ (Right solns) -> do
  let sorted =
- flip sortBy solns $ comparing $ \(ext, (_, holes)) ->
- Down $ scoreSolution ext jdg holes
+ flip sortBy solns $ comparing $ \(Proof ext _ holes) ->
+ Down $ scoreSolution ext jdg $ fmap snd holes
  case sorted of
- ((syn, (_, subgoals)) : _) ->
+ ((Proof syn _ subgoals) : _) ->
  Right $
  RunTacticResults
  { rtr_trace = syn_trace syn
  , rtr_extract = simplify $ syn_val syn
- , rtr_subgoals = subgoals
- , rtr_other_solns = reverse . fmap fst $ sorted
+ , rtr_subgoals = fmap snd subgoals
+ , rtr_other_solns = reverse . fmap pf_extract $ sorted
  , rtr_jdg = jdg
  , rtr_ctx = ctx
  }
@@ -154,7 +152,7 @@ mappingExtract
  -> TacticT jdg ext err s m a
 mappingExtract f (TacticT m)
  = TacticT $ StateT $ \jdg ->
- mapExtract' f $ runStateT m jdg
+ mapExtract id f $ runStateT m jdg
 
 
 ------------------------------------------------------------------------------
@@ -227,7 +225,10 @@ unify goal inst = do
  case tryUnifyUnivarsButNotSkolems skolems goal inst of
  Just subst ->
  modify $ updateSubst subst
- Nothing -> throwError (UnificationError inst goal)
+ Nothing -> cut -- failure (UnificationError inst goal)
+
+cut :: RuleT jdg ext err s m a
+cut = RuleT Empty
 
 
 ------------------------------------------------------------------------------
@@ -254,26 +255,6 @@ attemptWhen _ t2 False = t2
 attemptWhen t1 t2 True = commit t1 t2
 
 
-------------------------------------------------------------------------------
--- | Mystical time-traveling combinator for inspecting the extracts produced by
--- a tactic. We can use it to guard that extracts match certain predicates, for
--- example.
---
--- Note, that this thing is WEIRD. To illustrate:
---
--- @@
--- peek f
--- blah
--- @@
---
--- Here, @f@ can inspect the extract _produced by @blah@,_ which means the
--- causality appears to go backwards.
---
--- 'peek' should be exposed directly by @refinery@ in the next release.
-peek :: (ext -> TacticT jdg ext err s m ()) -> TacticT jdg ext err s m ()
-peek k = tactic $ \j -> Subgoal ((), j) $ \e -> proofState (k e) j
-
-
 ------------------------------------------------------------------------------
 -- | Run the given tactic iff the current hole contains no univars. Skolems and
 -- already decided univars are OK though.
@@ -284,7 +265,7 @@ requireConcreteHole m = do
  let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
  case S.size $ vars S.\\ skolems of
  0 -> m
- _ -> throwError TooPolymorphic
+ _ -> failure TooPolymorphic
 
 
 ------------------------------------------------------------------------------
@@ -317,7 +298,7 @@ useNameFromHypothesis f name = do
  hy <- jHypothesis <$> goal
  case M.lookup name $ hyByName hy of
  Just hi -> f hi
- Nothing -> throwError $ NotInScope name
+ Nothing -> failure $ NotInScope name
 
 ------------------------------------------------------------------------------
 -- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
@@ -326,7 +307,7 @@ useNameFromContext :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
 useNameFromContext f name = do
  lookupNameInContext name >>= \case
  Just ty -> f $ createImportedHyInfo name ty
- Nothing -> throwError $ NotInScope name
+ Nothing -> failure $ NotInScope name
 
 
 ------------------------------------------------------------------------------
@@ -340,12 +321,11 @@ lookupNameInContext name = do
 
 
 getDefiningType
- :: (MonadError TacticError m, MonadReader Context m)
- => m CType
+ :: TacticsM CType
 getDefiningType = do
  calling_fun_name <- fst . head <$> asks ctxDefiningFuncs
  maybe
- (throwError $ NotInScope calling_fun_name)
+ (failure $ NotInScope calling_fun_name)
  pure
  =<< lookupNameInContext calling_fun_name
 
@@ -403,7 +383,7 @@ getOccNameType
 getOccNameType occ = do
  getTyThing occ >>= \case
  Just (AnId v) -> pure $ varType v
- _ -> throwError $ NotInScope occ
+ _ -> failure $ NotInScope occ
 
 
 getCurrentDefinitions :: TacticsM [(OccName, CType)]

plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs

@@ -7,10 +7,12 @@
 module Wingman.Metaprogramming.Parser where
 
 import qualified Control.Monad.Combinators.Expr as P
-import qualified Control.Monad.Error.Class as E
 import Data.Functor
 import Data.Maybe (listToMaybe)
 import qualified Data.Text as T
+import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
+import FastString (unpackFS)
+import Refinery.Tactic (failure)
 import qualified Refinery.Tactic as R
 import qualified Text.Megaparsec as P
 import Wingman.Auto
@@ -20,8 +22,6 @@ import Wingman.Metaprogramming.Parser.Documentation
 import Wingman.Metaprogramming.ProofState (proofState, layout)
 import Wingman.Tactics
 import Wingman.Types
-import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
-import FastString (unpackFS)
 
 
 nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -296,7 +296,7 @@ commands =
  ( pure $
  fmap listToMaybe getCurrentDefinitions >>= \case
  Just (self, _) -> useNameFromContext (apply Saturated) self
- Nothing -> E.throwError $ TacticPanic "no defining function"
+ Nothing -> failure $ TacticPanic "no defining function"
  )
  [ Example
  (Just "In the context of `foo (a :: Int) (b :: b) = _`:")