Add yielding to help proof search

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Rules.elm

@@ -63,6 +63,9 @@ pure a env ps = Search.pure (a, ps)
 fail : Prover a
 fail env ps = Search.fail
 
+yield : Prover a -> Prover a
+yield p env ps = Search.yield (p env ps)
+
 getEnv : Prover RuleEnv
 getEnv env ps = Search.pure (env, ps)
 
@@ -110,7 +113,7 @@ provePremises = mapM proveTerm
 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
     getEnv
-    |> andThen (\env -> List.foldl (\r -> interleave (rule t r)) fail env.rules)
+    |> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
 
 prove : Term Metavariable -> Prover ProofTree
 prove mt =

src/Bergamot/Search.elm

@@ -1,8 +1,9 @@
-module Bergamot.Search exposing (Search, map, apply, andThen, pure, fail, interleave, one)
+module Bergamot.Search exposing (Search, map, apply, andThen, pure, fail, yield, interleave, one)
 
 type SearchStep a
     = Empty
     | Found a (Search a)
+    | Yield (Search a)
 
 type alias Search a = () -> SearchStep a
 
@@ -11,18 +12,21 @@ map f s () =
     case s () of
         Empty -> Empty
         Found a sp -> Found (f a) (map f sp)
+        Yield sp -> Yield (map f sp)
 
 apply : Search a -> Search (a -> b) -> Search b
 apply sa sf () =
     case sf () of
         Empty -> Empty
         Found f sfp -> interleave (map f sa) (apply sa sfp) ()
+        Yield sfp -> Yield (apply sa sfp)
 
 andThen : (a -> Search b) -> Search a -> Search b
 andThen f sa () =
     case sa () of
         Empty -> Empty
         Found a sap -> interleave (f a) (andThen f sap) ()
+        Yield sap -> Yield (andThen f sap)
 
 pure : a -> Search a
 pure a () = Found a (\() -> Empty)
@@ -30,14 +34,26 @@ pure a () = Found a (\() -> Empty)
 fail : Search a
 fail () = Empty
 
+yield : Search a -> Search a
+yield s () = Yield s
+
 interleave : Search a -> Search a -> Search a
 interleave s1 s2 () =
     case s1 () of
         Empty -> s2 ()
         Found a s1p -> Found a (interleave s2 s1p)
+        Yield s1p -> Yield (interleave s2 s1p)
 
 one : Search a -> Maybe (a, Search a)
 one s =
-    case s () of
-        Empty -> Nothing
-        Found a sp -> Just (a, sp)
+    let
+        go n sp =
+            if n > 0
+            then
+                case sp () of
+                    Empty -> Nothing
+                    Found a spp -> Just (a, spp)
+                    Yield spp -> go (n - 1) spp
+            else Nothing
+    in
+        go 10000 s

src/Main.elm

@@ -3,7 +3,7 @@ module Main exposing (main)
 import Browser
 import Html exposing (Html)
 import Html.Events exposing (onInput)
-import Html.Attributes exposing (type_, class)
+import Html.Attributes exposing (type_, class, value)
 import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
@@ -24,7 +24,7 @@ type Msg
     | SetQuery String
 
 init : Flags -> (Model, Cmd Msg)
-init () = ({ program = "", query = "" }, Cmd.none)
+init () = ({ program = "", query = "type(?e, tint)" }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -57,7 +57,7 @@ viewProofTree progs querys = viewSection "Proof Tree" <|
 view : Model -> Html Msg
 view m = Html.div [ class "elm-root" ]
     [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
-    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery ] []
+    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
     , viewRules m.program
     , viewProofTree m.program m.query
     ]