Upgrade to refinery-0.4.0.0 (#2021)

* Upgrade refinery versions

* Get everything compiling against refinery v4

* Don't use UnderlyingState

* Every test is fucked

* Update tests

Author: isovector

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) = _`:")