From 6271dd8c2ba8e1a75a2ce6df92f5da29fdb9dd06 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 26 Nov 2023 00:45:05 -0800
Subject: [PATCH] Add an initial implementation of proof search

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Rules.elm | 87 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 src/Bergamot/Rules.elm

diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
new file mode 100644
index 0000000..928e400
--- /dev/null
+++ b/src/Bergamot/Rules.elm
@@ -0,0 +1,87 @@
+module Bergamot.Rules exposing (..)
+
+import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState)
+import Bergamot.Search as Search exposing (Search)
+
+import Debug
+
+type alias Rule =
+    { name : String
+    , conclusion : Term Metavariable
+    , premises : List (Term Metavariable)
+    }
+
+type ProofTree = MkProofTree
+    { name : String
+    , conclusion : Term UnificationVar
+    , premises : List ProofTree
+    }
+
+type alias RuleEnv =
+    { rules : List Rule
+    }
+
+type alias ProveState =
+    { unificationState : UnificationState
+    , instantiationState : InstantiationState
+    }
+
+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)
+
+map : (a -> b) -> Prover a -> Prover b
+map f p env ps =
+    p env ps
+    |> Search.map (Tuple.mapFirst f)
+
+interleave : Prover a -> Prover a -> Prover a
+interleave p1 p2 env ps =
+    Search.interleave (p1 env ps) (p2 env ps)
+
+pure : a -> Prover a
+pure a env ps = Search.pure (a, ps)
+
+fail : Prover a
+fail env ps = Search.fail
+
+getEnv : Prover RuleEnv
+getEnv env ps = Search.pure (env, ps)
+
+rule : Term UnificationVar -> Rule -> Prover ProofTree
+rule t r env ps =
+    let
+        (conc, is) = instantiate r.conclusion ps.instantiationState
+        (prems, isp) = instantiateList r.premises is
+    in
+        case unify t conc ps.unificationState of
+            Nothing -> Search.fail
+            Just (tp, usp) ->
+                let
+                    psp = { ps | instantiationState = resetVars isp
+                               , unificationState = usp }
+                in
+                    provePremises prems env psp
+                    |> Search.map (Tuple.mapFirst (\trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees }))
+
+provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
+provePremises l =
+    case l of
+        t :: ts ->
+            prove t
+            |> andThen (\tree -> map (\trees -> tree :: trees) (provePremises ts))
+        [] -> pure []
+
+prove : Term UnificationVar -> Prover ProofTree
+prove t =
+    getEnv
+    |> andThen (List.foldl (\r -> interleave (rule t r)) fail << .rules)
+
+single : RuleEnv -> Prover a -> Maybe a
+single env p =
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState }
+    |> Search.one
+    |> Maybe.map (Tuple.first << Tuple.first)