Use 'gas' instead of yields to limit recursion

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

src/Bergamot/Rules.elm

@@ -24,6 +24,7 @@ type alias RuleEnv =
 type alias ProveState =
     { unificationState : UnificationState
     , instantiationState : InstantiationState
+    , gas: Int
     }
 
 type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
@@ -31,7 +32,7 @@ type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
 andThen : (a -> Prover b) -> Prover a -> Prover b
 andThen f p env ps =
     p env ps
-    |> Search.andThen (\(a, psp) -> (f a) env psp)
+    |> Search.andThen (\(a, psp) -> if psp.gas > 0 then (f a) env psp else Search.fail)
 
 join : Prover (Prover a) -> Prover a
 join p = andThen (\x -> x) p
@@ -72,6 +73,9 @@ getEnv env ps = Search.pure (env, ps)
 getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)
 
+burn : Prover ()
+burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
+
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
     let
@@ -112,7 +116,8 @@ provePremises = mapM proveTerm
 
 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
-    getEnv
+    burn
+    |> andThen (\() -> getEnv)
     |> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
 
 prove : Term Metavariable -> Prover ProofTree
@@ -122,6 +127,6 @@ prove mt =
 
 single : RuleEnv -> Prover a -> Maybe a
 single env p =
-    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState }
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
     |> Search.one
     |> Maybe.map (Tuple.first << Tuple.first)

src/Bergamot/Search.elm

@@ -46,14 +46,7 @@ interleave s1 s2 () =
 
 one : Search a -> Maybe (a, Search a)
 one s =
-    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
+    case s () of
+        Empty -> Nothing
+        Found a sp -> Just (a, sp)
+        Yield sp -> one sp