Add an interactive 'can this query be satisfied' interface

src/Bergamot/Rules.elm

@@ -90,16 +90,19 @@ provePremises l =
     case l of
         t :: ts ->
             pure (::)
-            |> apply (prove t)
+            |> apply (proveTerm t)
             |> apply (provePremises ts)
         [] -> pure []
 
+proveTerm : Term UnificationVar -> Prover ProofTree
+proveTerm t =
+    getEnv
+    |> andThen (\env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
+
 prove : Term Metavariable -> Prover ProofTree
 prove mt =
-    pure (\t env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
-    |> apply (liftInstantiation instantiate mt)
-    |> apply getEnv
-    |> join
+    liftInstantiation instantiate mt
+    |> andThen proveTerm
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =