@@ -160,3 +160,38 @@ inferType tac =
160 | err => fail [TextPart "Type inference failure"]
160 | err => fail [TextPart "Type inference failure"]
162 focus tmH
162 focus tmH
164+||| Given one tactic that produces a list of subgoal names and another
165+||| that produces some result, run the second tactic in each hole
166+||| produced by the first and return the resulting values.
168+||| Elab has no built-in notion of "subgoals", so this simulates the
169+||| Coq or JonPRL semicolon operators.
171+||| @ first run this tactic to produce subgoals
172+||| @ after run this tactic in each subgoal
173+andThen : (first : Elab (List TTName)) -> (after : Elab a) -> Elab (List a)
174+andThen first after =
176+ catMaybes <$> for hs (flip inHole after)
178+||| Refine the current goal using some term, constructing holes for
179+||| all arguments that can't be inferred. Return the list of generated
182+||| @ tm the term to apply to some number of goals
183+refine : (tm : Raw) -> Elab (List TTName)
185+ do ty <- (snd <$> check tm) >>= forgetTypes
188+ -- we don't care about negative results because it'll just fail anyway
189+ let argCount = minus (countPi ty) (countPi g)
190+ newHoles <- apply tm (replicate argCount (True, 0))
192+ actualHoles <- getHoles
193+ return (filter (flip elem actualHoles) (map snd newHoles))
195+ where countPi : Raw -> Nat
196+ countPi (RBind _ (Pi _ _) body) = S (countPi body)