@@ -160,3 +160,38 @@ inferType tac =
160160 | err => fail [TextPart "Type inference failure"]
161161 solve
162162 focus tmH
163+
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.
167+|||
168+||| Elab has no built-in notion of "subgoals", so this simulates the
169+||| Coq or JonPRL semicolon operators.
170+|||
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 =
175+ do hs <- first
176+ catMaybes <$> for hs (flip inHole after)
177+
178+||| Refine the current goal using some term, constructing holes for
179+||| all arguments that can't be inferred. Return the list of generated
180+||| holes.
181+|||
182+||| @ tm the term to apply to some number of goals
183+refine : (tm : Raw) -> Elab (List TTName)
184+refine tm =
185+ do ty <- (snd <$> check tm) >>= forgetTypes
186+ g <- goalType
187+
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))
191+ solve
192+ actualHoles <- getHoles
193+ return (filter (flip elem actualHoles) (map snd newHoles))
194+
195+ where countPi : Raw -> Nat
196+ countPi (RBind _ (Pi _ _) body) = S (countPi body)
197+ countPi _ = Z