From e123f24af09535d359c0fbc8a722120b703c7858 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 26 Nov 2023 13:14:44 -0800
Subject: [PATCH] Add support for reifying proof trees

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Rules.elm | 29 +++++++++++++++++++++--------
 src/Main.elm           |  2 +-
 2 files changed, 22 insertions(+), 9 deletions(-)

diff --git a/src/Bergamot/Rules.elm b/src/Bergamot/Rules.elm
index a384f4c..c84215d 100644
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -1,6 +1,6 @@
 module Bergamot.Rules exposing (..)
 
-import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState)
+import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
 import Bergamot.Search as Search exposing (Search)
 
 import Debug
@@ -44,6 +44,15 @@ map f p env ps =
     p env ps
     |> Search.map (Tuple.mapFirst f)
 
+mapM : (a -> Prover b) -> List a -> Prover (List b)
+mapM f l =
+    case l of
+        x :: xs ->
+            pure (::)
+            |> apply (f x)
+            |> apply (mapM f xs)
+        [] -> pure []
+
 interleave : Prover a -> Prover a -> Prover a
 interleave p1 p2 env ps =
     Search.interleave (p1 env ps) (p2 env ps)
@@ -57,6 +66,9 @@ fail env ps = Search.fail
 getEnv : Prover RuleEnv
 getEnv env ps = Search.pure (env, ps)
 
+getUnificationState : Prover UnificationState
+getUnificationState env ps = Search.pure (ps.unificationState, ps)
+
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
     let
@@ -75,6 +87,13 @@ withVars p env ps =
     p env ps
     |> Search.map (Tuple.mapSecond (\psp -> { psp | instantiationState = resetVars psp.instantiationState }))
 
+
+reifyProofTree : ProofTree -> Prover ProofTree
+reifyProofTree (MkProofTree node) =
+    pure (\t trees -> MkProofTree { node | conclusion = t, premises = trees })
+    |> apply (map (reify node.conclusion) getUnificationState)
+    |> apply (mapM reifyProofTree node.premises)
+
 rule : Term UnificationVar -> Rule -> Prover ProofTree
 rule t r =
         withVars (pure Tuple.pair
@@ -86,13 +105,7 @@ rule t r =
             |> apply (provePremises prems))
 
 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
-provePremises l =
-    case l of
-        t :: ts ->
-            pure (::)
-            |> apply (proveTerm t)
-            |> apply (provePremises ts)
-        [] -> pure []
+provePremises = mapM proveTerm
 
 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
diff --git a/src/Main.elm b/src/Main.elm
index 0921c0e..54c603e 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -27,7 +27,7 @@ init () = ({ program = "", query = "" }, Cmd.none)
 proveQuery : String -> String -> Maybe ProofTree
 proveQuery progs querys =
     case (run program progs, run term querys) of
-        (Just prog, Just query) -> single prog (prove query)
+        (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
 view : Model -> Html Msg