Clean up inference in Pruviloj

Now, the proper Infer type is used, and a tactic is exported.

libs/pruviloj/Pruviloj/Core.idr

@@ -3,13 +3,8 @@
 ||| eventual Prelude inclusion.
 module Pruviloj.Core
 
-
-import Language.Reflection.Elab
 import Language.Reflection.Utils
 
-data Infer : Type where
-  MkInfer : (a : Type) -> a -> Infer
-
 ||| Run something for effects, throwing away the return value
 ignore : Functor f => f a -> f ()
 ignore x = map (const ()) x
@@ -85,11 +80,11 @@ intros = do g <- snd <$> getGoal
 
 ||| Run a tactic inside of a particular hole, if it still exists. If
 ||| it has been solved, do nothing.
-inHole : TTName -> Elab () -> Elab ()
+inHole : TTName -> Elab a -> Elab (Maybe a)
 inHole h todo =
-  when (h `elem` !getHoles) $
-    do focus h
-       todo
+  if (h `elem` !getHoles)
+    then do focus h; Just <$> todo
+    else return Nothing
 
 ||| Restrict a polymorphic type to () for contexts where it doesn't
 ||| matter. This is nice for sticking `debug` in a context where
@@ -142,3 +137,26 @@ bindPat = do compute
              case g of
                Bind n (PVTy _) _ => patbind n
                _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
+
+||| The underlying implementation type for the inferType operator.
+data Infer : Type where
+  MkInfer : (a : Type) -> a -> Infer
+
+||| Run a tactic script in a context where the type of the resulting
+||| expression must be solvable via unification. Return the term and
+||| its type.
+|||
+||| @ tac a tactic script that will be run with focus on the hole
+|||       whose type is to be inferred.
+total
+inferType : (tac : Elab ()) -> Elab (TT, TT)
+inferType tac =
+    case fst !(runElab `(Infer) (startInfer *> tac)) of
+        `(MkInfer ~ty ~tm) => return (tm, ty)
+        _ => fail [TextPart "Not infer"]
+  where
+    startInfer : Elab ()
+    startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]
+                       | err => fail [TextPart "Type inference failure"]
+                    solve
+                    focus tmH

libs/pruviloj/Pruviloj/Internals.idr

@@ -77,10 +77,6 @@ enumerate xs = enumerate' xs 0
         enumerate' [] _ = []
         enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
 
-getSigmaArgs : Raw -> Elab (Raw, Raw)
-getSigmaArgs `(MkSigma {a=~_} {P=~_} ~rhsTy ~lhs) = return (rhsTy, lhs)
-getSigmaArgs arg = fail [TextPart "Not a sigma constructor"]
-
 bindPats : List (TTName, Binder Raw) -> Raw -> Raw
 bindPats [] res = res
 bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
@@ -109,19 +105,19 @@ partial
 elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
 elabPatternClause lhs rhs =
   do -- Elaborate the LHS in a context where its type will be solved via unification
-     (pat, _) <- runElab `(Sigma Type id) $
+     (pat, _) <- runElab `(Infer) $
                     do th <- newHole "finalTy" `(Type)
                        patH <- newHole "pattern" (Var th)
-                       fill `(MkSigma ~(Var th) ~(Var patH) : Sigma Type id)
+                       fill `(MkInfer ~(Var th) ~(Var patH))
                        solve
                        focus patH
                        lhs
                        -- Convert all remaining holes to pattern variables
                        traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
-     let (pvars, sigma) = extractBinders !(forgetTypes pat)
-     (rhsTy, lhsTm) <- getSigmaArgs sigma
+     (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forgetTypes pat)
+        | fail [TextPart "Couldn't infer type of left-hand pattern"]
      rhsTm <- runElab (bindPatTys pvars rhsTy) $
-                                  do -- Introduce all the pattern variables from the LHS
+                do -- Introduce all the pattern variables from the LHS
                    repeatUntilFail bindPat <|> return ()
                    rhs
      realRhs <- forgetTypes (fst rhsTm)