From 12d823e944c3a68ba5273e9ba78e1bad7728a7a0 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 22 Dec 2023 15:58:52 -0800
Subject: [PATCH] Configure prommpts via a Bergamot program, too.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Bergamot/Syntax.elm |  1 +
 src/Main.elm            | 39 +++++++++++++++++++++++++++------------
 2 files changed, 28 insertions(+), 12 deletions(-)

diff --git a/src/Bergamot/Syntax.elm b/src/Bergamot/Syntax.elm
index 43a9d57..403fefa 100644
--- a/src/Bergamot/Syntax.elm
+++ b/src/Bergamot/Syntax.elm
@@ -1,5 +1,6 @@
 module Bergamot.Syntax exposing
     ( Term(..), map, andThen, Metavariable(..), UnificationVar(..)
+    , unMetavariable, unUnificationVar
     , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
     , unify, unifyList, UnificationState, emptyUnificationState
     , reify
diff --git a/src/Main.elm b/src/Main.elm
index c17209a..51b1135 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -54,12 +54,13 @@ resultModeEq rm1 rm2 =
 type alias Model =
     { program : String
     , renderProgram: String
+    , inputProgram : String
     , tab : Tab
     , query : String
     , editMode : EditMode
     , resultMode : ResultMode
     }
-type alias Flags = { renderRules: String, rules: String, query: String }
+type alias Flags = { renderRules: String, inputRules: String, rules: String, query: String }
 type Msg
     = SetProgram String
     | SetRenderProgram String
@@ -69,7 +70,7 @@ type Msg
     | SetResultMode ResultMode
 
 init : Flags -> (Model, Cmd Msg)
-init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
+init fs = ({ program = fs.rules, renderProgram = fs.renderRules, inputProgram = fs.inputRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
 
 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
@@ -121,22 +122,36 @@ viewRules renderProgs progs =
             (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
             _ -> []
 
-proofGoal : EditMode -> String -> Maybe (Term Metavariable)
-proofGoal editMode querys =
+proofGoal : EditMode -> String -> String -> Maybe (Term Metavariable)
+proofGoal editMode inputProgs querys =
     case editMode of
         Query -> run term querys
-        Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
+        Syntax ->
+            case (run program inputProgs, run parseExpr querys) of
+                (Just inputProg, Just e) ->
+                    let
+                        inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] }
+                        fullProgram = { sections = { name = "", rules = [inputRule] } :: inputProg.sections }
+                        query = Call "prompt" [Var (MkMetavariable "?p")]
+                    in
+                        case single fullProgram (prove query |> Bergamot.Rules.andThen reifyProofTree) of
+                            Just (MkProofTree node) ->
+                                case node.conclusion of
+                                    Call "prompt" [t] -> Just <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
+                                    _ -> Nothing
+                            _ -> Nothing
+                _ -> Nothing
 
-tryProve : EditMode -> String -> String -> Maybe ProofTree
-tryProve editMode progs querys =
-    case (run program progs, proofGoal editMode querys) of
+tryProve : EditMode -> String -> String -> String -> Maybe ProofTree
+tryProve editMode inputProgs progs querys =
+    case (run program progs, proofGoal editMode inputProgs querys) of
         (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
         _ -> Nothing
 
-viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg
-viewProofTree editMode resultMode renderProgs progs querys =
+viewProofTree : EditMode -> ResultMode -> String -> String -> String -> String -> Html Msg
+viewProofTree editMode resultMode renderProgs inputProgs progs querys =
     Html.div [ class "bergamot-proof-tree" ] <|
-        case tryProve editMode progs querys of
+        case tryProve editMode inputProgs progs querys of
             Just (MkProofTree tree) ->
                 case run program renderProgs of
                     Just renderProg ->
@@ -158,7 +173,7 @@ view m = Html.div [ class "bergamot-root" ]
         ]
     , viewSection "Result" <| Html.div[]
         [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
-        , viewProofTree m.editMode m.resultMode m.renderProgram m.program m.query
+        , viewProofTree m.editMode m.resultMode m.renderProgram m.inputProgram m.program m.query
         ]
     , viewSection "Rules" <| Html.div []
         [ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]