Wingman: Tactical support for deep recursion (#1944)

* Make `try` a tactic combinator instead of an operator

* wip

* with_arg and deep_of

* Tactic arguments require parentheses

* Add deep_of test

* Fix MetaTry

* Haddock

* with_arg test

* It was a stupid inside joke

Author: isovector

plugins/hls-tactics-plugin/COMMANDS.md

@@ -23,6 +23,7 @@ running  `application` will produce:
 ```haskell
 f (_ :: a)
 ```
+
 ## apply
 
 arguments: single reference.  
@@ -46,6 +47,7 @@ running  `apply f` will produce:
 ```haskell
 f (_ :: a)
 ```
+
 ## assume
 
 arguments: single reference.  
@@ -69,6 +71,7 @@ running  `assume some_a_val` will produce:
 ```haskell
 some_a_val
 ```
+
 ## assumption
 
 arguments: none.  
@@ -92,6 +95,7 @@ running  `assumption` will produce:
 ```haskell
 some_a_val
 ```
+
 ## auto
 
 arguments: none.  
@@ -116,6 +120,7 @@ running  `auto` will produce:
 ```haskell
 g . f
 ```
+
 ## binary
 
 arguments: none.  
@@ -139,6 +144,7 @@ running  `binary` will produce:
 ```haskell
 (_3 :: a -> a -> Int) (_1 :: a) (_2 :: a)
 ```
+
 ## cata
 
 arguments: single reference.  
@@ -168,6 +174,7 @@ case x of
         a2_c = f a2
      in _
 ```
+
 ## collapse
 
 arguments: none.  
@@ -193,6 +200,7 @@ running  `collapse` will produce:
 ```haskell
 (_ :: a -> a -> a -> a) a1 a2 a3
 ```
+
 ## ctor
 
 arguments: single reference.  
@@ -214,6 +222,7 @@ running  `ctor Just` will produce:
 ```haskell
 Just (_ :: a)
 ```
+
 ## destruct
 
 arguments: single reference.  
@@ -239,6 +248,7 @@ case a of
   False -> _
   True -> _
 ```
+
 ## destruct_all
 
 arguments: none.  
@@ -271,6 +281,7 @@ case a of
     Nothing -> _
     Just i -> _
 ```
+
 ## homo
 
 arguments: single reference.  
@@ -298,6 +309,7 @@ case e of
   Left a -> Left (_ :: x)
   Right b -> Right (_ :: y)
 ```
+
 ## intro
 
 arguments: single binding.  
@@ -319,6 +331,7 @@ running  `intro aye` will produce:
 ```haskell
 \aye -> (_ :: b -> c -> d)
 ```
+
 ## intros
 
 arguments: varadic binding.  
@@ -368,6 +381,29 @@ running  `intros x y z w` will produce:
 ```haskell
 \x y z -> (_ :: d)
 ```
+
+## nested
+
+arguments: single reference.  
+non-deterministic.
+
+> Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context.
+
+
+### Example
+
+Given:
+
+```haskell
+_ :: [(Int, Either Bool a)] -> [(Int, Either Bool b)]
+```
+
+running  `nested fmap` will produce:
+
+```haskell
+fmap (fmap (fmap _))
+```
+
 ## obvious
 
 arguments: none.  
@@ -389,6 +425,7 @@ running  `obvious` will produce:
 ```haskell
 []
 ```
+
 ## pointwise
 
 arguments: tactic.  
@@ -412,6 +449,7 @@ running  `pointwise (use mappend)` will produce:
 ```haskell
 mappend _ _
 ```
+
 ## recursion
 
 arguments: none.  
@@ -435,6 +473,7 @@ running  `recursion` will produce:
 ```haskell
 foo (_ :: Int) (_ :: b)
 ```
+
 ## sorry
 
 arguments: none.  
@@ -456,6 +495,7 @@ running  `sorry` will produce:
 ```haskell
 _ :: b
 ```
+
 ## split
 
 arguments: none.  
@@ -477,6 +517,38 @@ running  `split` will produce:
 ```haskell
 Right (_ :: b)
 ```
+
+## try
+
+arguments: tactic.  
+non-deterministic.
+
+> Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states.
+
+
+### Example
+
+Given:
+
+```haskell
+f :: a -> b
+
+_ :: b
+```
+
+running  `try (apply f)` will produce:
+
+```haskell
+-- BOTH of:
+
+f (_ :: a)
+
+-- and
+
+_ :: b
+
+```
+
 ## unary
 
 arguments: none.  
@@ -500,6 +572,7 @@ running  `unary` will produce:
 ```haskell
 (_2 :: a -> Int) (_1 :: a)
 ```
+
 ## use
 
 arguments: single reference.  
@@ -523,3 +596,28 @@ running  `use isSpace` will produce:
 ```haskell
 isSpace (_ :: Char)
 ```
+
+## with_arg
+
+arguments: none.  
+deterministic.
+
+> Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context.
+
+
+### Example
+
+> Where `a` is a new unifiable type variable.
+
+Given:
+
+```haskell
+_ :: r
+```
+
+running  `with_arg` will produce:
+
+```haskell
+(_2 :: a -> r) (_1 :: a)
+```
+

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

@@ -113,7 +113,7 @@ freshTyvars t = do
         case M.lookup tv reps of
           Just tv' -> tv'
           Nothing  -> tv
-      ) t
+      ) $ snd $ tcSplitForAllTys t
 
 
 ------------------------------------------------------------------------------

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

@@ -35,7 +35,7 @@ deriveFmap = do
   try intros
   overAlgebraicTerms homo
   choice
-    [ overFunctions apply >> auto' 2
+    [ overFunctions (apply Saturated) >> auto' 2
     , assumption
     , recursion
     ]

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

@@ -188,7 +188,7 @@ commands =
 
   , command "apply" Deterministic (Ref One)
       "Apply the given function from *local* scope."
-      (pure . useNameFromHypothesis apply)
+      (pure . useNameFromHypothesis (apply Saturated))
       [ Example
           Nothing
           ["f"]
@@ -295,7 +295,7 @@ commands =
       "Fill the current hole with a call to the defining function."
       ( pure $
           fmap listToMaybe getCurrentDefinitions >>= \case
-            Just (self, _) -> useNameFromContext apply self
+            Just (self, _) -> useNameFromContext (apply Saturated) self
             Nothing -> E.throwError $ TacticPanic "no defining function"
       )
       [ Example
@@ -308,13 +308,7 @@ commands =
 
   , command "use" Deterministic (Ref One)
       "Apply the given function from *module* scope."
-      ( \occ -> pure $ do
-          ctx <- ask
-          ty <- case lookupNameInContext occ ctx of
-            Just ty -> pure ty
-            Nothing -> CType <$> getOccNameType occ
-          apply $ createImportedHyInfo occ ty
-      )
+      (pure . use Saturated)
       [ Example
           (Just "`import Data.Char (isSpace)`")
           ["isSpace"]
@@ -354,6 +348,44 @@ commands =
           "(_ :: a -> a -> a -> a) a1 a2 a3"
       ]
 
+  , command "try" Nondeterministic Tactic
+      "Simultaneously run and do not run a tactic. Subsequent tactics will bind on both states."
+      (pure . R.try)
+      [ Example
+          Nothing
+          ["(apply f)"]
+          [ EHI "f" "a -> b"
+          ]
+          (Just "b")
+          $ T.pack $ unlines
+            [ "-- BOTH of:\n"
+            , "f (_ :: a)"
+            , "\n-- and\n"
+            , "_ :: b"
+            ]
+      ]
+
+  , command "nested" Nondeterministic (Ref One)
+      "Nest the given function (in module scope) with itself arbitrarily many times. NOTE: The resulting function is necessarily unsaturated, so you will likely need `with_arg` to use this tactic in a saturated context."
+      (pure . nested)
+      [ Example
+          Nothing
+          ["fmap"]
+          []
+          (Just "[(Int, Either Bool a)] -> [(Int, Either Bool b)]")
+          "fmap (fmap (fmap _))"
+      ]
+
+  , command "with_arg" Deterministic Nullary
+      "Fill the current goal with a function application. This can be useful when you'd like to fill in the argument before the function, or when you'd like to use a non-saturated function in a saturated context."
+      (pure with_arg)
+      [ Example
+          (Just "Where `a` is a new unifiable type variable.")
+          []
+          []
+          (Just "r")
+          "(_2 :: a -> r) (_1 :: a)"
+      ]
   ]
 
 
@@ -369,14 +401,9 @@ oneTactic =
 tactic :: Parser (TacticsM ())
 tactic = flip P.makeExprParser operators oneTactic
 
-bindOne :: TacticsM a -> TacticsM a -> TacticsM a
-bindOne t t1 = t R.<@> [t1]
-
 operators :: [[P.Operator Parser (TacticsM ())]]
 operators =
-    [ [ P.Prefix (symbol "*"   $> R.many_) ]
-    , [ P.Prefix (symbol "try" $> R.try) ]
-    , [ P.InfixR (symbol "|"   $> (R.<%>) )]
+    [ [ P.InfixR (symbol "|"   $> (R.<%>) )]
     , [ P.InfixL (symbol ";"   $> (>>))
       , P.InfixL (symbol ","   $> bindOne)
       ]
@@ -426,7 +453,7 @@ parseMetaprogram
 -- | Automatically generate the metaprogram command reference.
 writeDocumentation :: IO ()
 writeDocumentation =
-  writeFile "plugins/hls-tactics-plugin/COMMANDS.md" $
+  writeFile "COMMANDS.md" $
     unlines
       [ "# Wingman Metaprogram Command Reference"
       , ""

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

@@ -150,6 +150,7 @@ prettyCommand (MC name syn det desc _ exs) = vsep
   , ">" <+> align (pretty desc)
   , mempty
   , vsep $ fmap (prettyExample name) exs
+  , mempty
   ]