Refactor tactics to track hypothesis provenance (#557)

This PR greatly simplifies the Judgement type, removing several pieces of denormalized state that were a headache to keep synchronized (and, as it happens, weren't!). The core change here is a new type Provenance, which tracks where a term came from, and thus what we're allowed to do with it. The result is a significantly more maintainable implementation.

Author: isovector

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -22,9 +22,11 @@ import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
+import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
 import           Data.List
+import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
@@ -214,7 +216,7 @@ filterBindingType
 filterBindingType p tp dflags plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
-   in fmap join $ for (M.toList hy) $ \(occ, CType ty) ->
+   in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->
         case p (unCType g) ty of
           True  -> tp occ ty dflags plId uri range jdg
           False -> pure []
@@ -264,23 +266,28 @@ judgementForHole state nfp range = do
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
               tcg
-      hyps = hypothesisFromBindings rss binds
-      ambient = M.fromList $ contextMethodHypothesis ctx
+      top_provs = getRhsPosVals rss tcs
+      local_hy = spliceProvenance top_provs
+               $ hypothesisFromBindings rss binds
+      cls_hy = contextMethodHypothesis ctx
   pure ( resulting_range
        , mkFirstJudgement
-           hyps
-           ambient
+           (local_hy <> cls_hy)
            (isRhsHole rss tcs)
-           (maybe
-              mempty
-              (uncurry M.singleton . fmap pure)
-                $ getRhsPosVals rss tcs)
            goal
        , ctx
        , dflags
        )
 
 
+spliceProvenance
+    :: Map OccName Provenance
+    -> Map OccName (HyInfo a)
+    -> Map OccName (HyInfo a)
+spliceProvenance provs =
+  M.mapWithKey $ \name hi ->
+    overProvenance (maybe id const $ M.lookup name provs) hi
+
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
 tacticCmd tac lf state (TacticParams uri range var_name)
@@ -334,17 +341,22 @@ isRhsHole rss tcs = everything (||) (mkQ False $ \case
 
 ------------------------------------------------------------------------------
 -- | Compute top-level position vals of a function
-getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
-getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
-  TopLevelRHS name ps
-      (L (RealSrcSpan span)  -- body with no guards and a single defn
-         (HsVar _ (L _ hole)))
-    | containsSpan rss span  -- which contains our span
-    , isHole $ occName hole  -- and the span is a hole
-    -> First $ do
-        patnames <- traverse getPatName ps
-        pure (occName name, patnames)
-  _ -> mempty
+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance
+getRhsPosVals rss tcs
+  = M.fromList
+  $ join
+  $ maybeToList
+  $ getFirst
+  $ everything (<>) (mkQ mempty $ \case
+      TopLevelRHS name ps
+          (L (RealSrcSpan span)  -- body with no guards and a single defn
+            (HsVar _ (L _ hole)))
+        | containsSpan rss span  -- which contains our span
+        , isHole $ occName hole  -- and the span is a hole
+        -> First $ do
+            patnames <- traverse getPatName ps
+            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name
+      _ -> mempty
   ) tcs
 
 

plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs

@@ -23,6 +23,6 @@ auto = do
   commit knownStrategies
     . tracing "auto"
     . localTactic (auto' 4)
-    . disallowing
+    . disallowing RecursiveCall
     $ fmap fst current
 

plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

@@ -43,8 +43,8 @@ useOccName jdg name =
 
 ------------------------------------------------------------------------------
 -- | Doing recursion incurs a small penalty in the score.
-penalizeRecursion :: MonadState TacticState m => m ()
-penalizeRecursion = modify $ field @"ts_recursion_penality" +~ 1
+countRecursiveCall :: TacticState -> TacticState
+countRecursiveCall = field @"ts_recursion_count" +~ 1
 
 
 ------------------------------------------------------------------------------
@@ -57,14 +57,14 @@ addUnusedTopVals vals = modify $ field @"ts_unused_top_vals" <>~ vals
 destructMatches
     :: (DataCon -> Judgement -> Rule)
        -- ^ How to construct each match
-    -> ([(OccName, CType)] -> Judgement -> Judgement)
-       -- ^ How to derive each match judgement
+    -> Maybe OccName
+       -- ^ Scrutinee
     -> CType
        -- ^ Type being destructed
     -> Judgement
     -> RuleM (Trace, [RawMatch])
-destructMatches f f2 t jdg = do
-  let hy = jHypothesis jdg
+destructMatches f scrut t jdg = do
+  let hy = jEntireHypothesis jdg
       g  = jGoal jdg
   case splitTyConApp_maybe $ unCType t of
     Nothing -> throwError $ GoalMismatch "destruct" g
@@ -76,11 +76,7 @@ destructMatches f f2 t jdg = do
           let args = dataConInstOrigArgTys' dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
-              dcon_name = nameOccName $ dataConName dc
-
-          let j = f2 hy'
-                $ withPositionMapping dcon_name names
-                $ introducingPat hy'
+              j = introducingPat scrut dc hy'
                 $ withNewGoal g jdg
           (tr, sg) <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
@@ -142,14 +138,14 @@ destruct' f term jdg = do
   let hy = jHypothesis jdg
   case find ((== term) . fst) $ toList hy of
     Nothing -> throwError $ UndefinedHypothesis term
-    Just (_, t) -> do
+    Just (_, hi_type -> t) -> do
       useOccName jdg term
       (tr, ms)
           <- destructMatches
                f
-               (\cs -> setParents term (fmap fst cs) . destructing term)
+               (Just term)
                t
-               jdg
+               $ disallowing AlreadyDestructed [term] jdg
       pure ( rose ("destruct " <> show term) $ pure tr
            , noLoc $ case' (var' term) ms
            )
@@ -165,7 +161,7 @@ destructLambdaCase' f jdg = do
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
       fmap (fmap noLoc $ lambdaCase) <$>
-        destructMatches f (const id) (CType arg) jdg
+        destructMatches f Nothing (CType arg) jdg
     _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
 
@@ -178,12 +174,11 @@ buildDataCon
     -> RuleM (Trace, LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstOrigArgTys' dc apps
-      dcon_name = nameOccName $ dataConName dc
   (tr, sgs)
       <- fmap unzipTrace
        $ traverse ( \(arg, n) ->
                     newSubgoal
-                  . filterSameTypeFromOtherPositions dcon_name n
+                  . filterSameTypeFromOtherPositions dc n
                   . blacklistingDestruct
                   . flip withNewGoal jdg
                   $ CType arg

plugins/tactics/src/Ide/Plugin/Tactic/Context.hs

@@ -7,6 +7,8 @@ import           Bag
 import           Control.Arrow
 import           Control.Monad.Reader
 import           Data.List
+import           Data.Map (Map)
+import qualified Data.Map as M
 import           Data.Maybe (mapMaybe)
 import           Data.Set (Set)
 import qualified Data.Set as S
@@ -33,9 +35,10 @@ mkContext locals tcg = Context
 
 ------------------------------------------------------------------------------
 -- | Find all of the class methods that exist from the givens in the context.
-contextMethodHypothesis :: Context -> [(OccName, CType)]
+contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)
 contextMethodHypothesis ctx
-  = excludeForbiddenMethods
+  = M.fromList
+  . excludeForbiddenMethods
   . join
   . concatMap
       ( mapMaybe methodHypothesis
@@ -51,7 +54,7 @@ contextMethodHypothesis ctx
 -- | Many operations are defined in typeclasses for performance reasons, rather
 -- than being a true part of the class. This function filters out those, in
 -- order to keep our hypothesis space small.
-excludeForbiddenMethods :: [(OccName, CType)] -> [(OccName, CType)]
+excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]
 excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
   where
     forbiddenMethods :: Set OccName