@@ -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,26 @@ 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