From 535c714b47c1cd23acabc6926b5a9cdfed5a7942 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 21 Dec 2023 16:47:56 -0800 Subject: [PATCH] Remove yields and switch to depth-based gas. This considerably speeds up forward inference, but we do get lost when trying to prove more difficult things, or doing backwards search. Signed-off-by: Danila Fedorin --- src/Bergamot/Rules.elm | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm index ab00fe9..70486ac 100644 --- a/src/Bergamot/Rules.elm +++ b/src/Bergamot/Rules.elm @@ -82,8 +82,8 @@ getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps) getUnificationState : Prover UnificationState getUnificationState env ps = Search.pure (ps.unificationState, ps) -burn : Prover () -burn env ps = if ps.gas > 0 then Search.pure ((), { ps | gas = ps.gas - 1}) else Search.fail +burn : Prover a -> Prover a +burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b liftInstantiation f a env ps = @@ -171,9 +171,9 @@ proveTerm : Term UnificationVar -> Prover ProofTree proveTerm t = map (reify t) getUnificationState |> andThen (\tp -> - burn - |> andThen (\() -> getRules) - |> andThen (List.foldl (\r -> interleave (yield (rule tp r))) (builtinRules tp))) + burn ( + getRules + |> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp)))) prove : Term Metavariable -> Prover ProofTree prove mt = @@ -182,6 +182,6 @@ prove mt = single : RuleEnv -> Prover a -> Maybe a single env p = - p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 } + p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 30 } |> Search.one |> Maybe.map (Tuple.first << Tuple.first)