@@ -3,13 +3,8 @@
33||| eventual Prelude inclusion.
44module Pruviloj.Core
55
6−
7−import Language.Reflection.Elab
86import Language.Reflection.Utils
97
10−data Infer : Type where
11− MkInfer : (a : Type) -> a -> Infer
12−
138||| Run something for effects, throwing away the return value
149ignore : Functor f => f a -> f ()
1510ignore x = map (const ()) x
@@ -85,11 +80,11 @@ intros = do g <- snd <$> getGoal
8580
8681||| Run a tactic inside of a particular hole, if it still exists. If
8782||| it has been solved, do nothing.
88−inHole : TTName -> Elab () -> Elab ()
83+inHole : TTName -> Elab a -> Elab (Maybe a)
8984inHole h todo =
90− when (h `elem` !getHoles) $
91− do focus h
92− todo
85+ if (h `elem` !getHoles)
86+ then do focus h; Just <$> todo
87+ else return Nothing
9388
9489||| Restrict a polymorphic type to () for contexts where it doesn't
9590||| matter. This is nice for sticking `debug` in a context where
@@ -142,3 +137,89 @@ bindPat = do compute
142137 case g of
143138 Bind n (PVTy _) _ => patbind n
144139 _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
140+
141+||| The underlying implementation type for the inferType operator.
142+data Infer : Type where
143+ MkInfer : (a : Type) -> a -> Infer
144+
145+||| Run a tactic script in a context where the type of the resulting
146+||| expression must be solvable via unification. Return the term and
147+||| its type.
148+|||
149+||| @ tac a tactic script that will be run with focus on the hole
150+||| whose type is to be inferred.
151+total
152+inferType : (tac : Elab ()) -> Elab (TT, TT)
153+inferType tac =
154+ case fst !(runElab `(Infer) (startInfer *> tac)) of
155+ `(MkInfer ~ty ~tm) => return (tm, ty)
156+ _ => fail [TextPart "Not infer"]
157+ where
158+ startInfer : Elab ()
159+ startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]
160+ | err => fail [TextPart "Type inference failure"]
161+ solve
162+ 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
198+
199+
200+||| Split a pair into its projections, binding them in the context
201+||| with the supplied names. A special case of Coq's `inversion`.
202+both : Raw -> TTName -> TTName -> Elab ()
203+both tm n1 n2 =
204+ do -- We don't know that the term is canonical, so let-bind projections applied to it
205+ (A, B) <- isPairTy (snd !(check tm))
206+ remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
207+ remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
208+ where
209+ isPairTy : TT -> Elab (Raw, Raw)
210+ isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]
211+ isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]
212+
213+||| Let-bind all results of completely destructuring nested tuples.
214+|||
215+||| This makes them available to the `hypothesis` tactic, among others.
216+|||
217+||| @ tm the nested tuple to destructure
218+covering
219+unproduct : (tm : Raw) -> Elab ()
220+unproduct tm =
221+ do n1 <- gensym "left"
222+ n2 <- gensym "right"
223+ both tm n1 n2
224+ try (unproduct (Var n1))
225+ try (unproduct (Var n2))