From 84c79ddb507701a25e8cf00114fdd2c33aa98e53 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 21 Dec 2023 14:06:37 -0800
Subject: [PATCH] Render sections in widget

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 src/Main.elm | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/Main.elm b/src/Main.elm
index 0b83c1a..458eef7 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -11,6 +11,7 @@ import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
 import Bergamot.ObjectLanguage exposing (..)
+import Bergamot.Utils exposing (..)
 import Json.Encode
 import Maybe
 import Tuple
@@ -83,18 +84,28 @@ viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
 viewRule env r = renderRuleViaRules env r
     |> Maybe.map latex
 
+viewRuleSection : RuleEnv -> Section -> Maybe (Html Msg)
+viewRuleSection env sec =
+    List.map (viewRule env) sec.rules
+    |> sequenceMaybes
+    |> Maybe.map (\rs ->
+        Html.div [ class "bergamot-rule-section" ]
+        [ Html.div [ class "bergamot-rule-list" ] rs
+        , Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
+        ])
+
 viewRules : String -> String -> Html Msg
 viewRules renderProgs progs = viewSection "Rendered Rules" <|
-    Html.div [ class "bergamot-rule-list" ] <|
+    Html.div [ class "bergamot-section-list" ] <|
         case (run program renderProgs, run program progs) of
-            (Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) (List.concatMap .rules prog.sections)
+            (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
             _ -> []
 
 proofGoal : EditMode -> String -> Maybe (Term Metavariable)
 proofGoal mode querys =
     case mode of
         Query -> run term querys
-        Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
+        Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
 
 tryProve : EditMode -> String -> String -> Maybe ProofTree
 tryProve mode progs querys =
@@ -114,11 +125,11 @@ view : Model -> Html Msg
 view m = Html.div [ class "bergamot-root" ]
     [ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
     , viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
+    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
+    , viewProofTree m.editMode m.program m.query
     , viewTab m.tab
         (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
         (Html.Lazy.lazy2 viewRules m.renderProgram m.program)
-    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
-    , viewProofTree m.editMode m.program m.query
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)