diff --git a/index.html b/index.html
index 9ec0c9c..feee0b7 100644
--- a/index.html
+++ b/index.html
@@ -2,10 +2,45 @@
+
Main
+
diff --git a/src/Main.elm b/src/Main.elm
index 53567a6..f610185 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -3,7 +3,7 @@ module Main exposing (main)
import Browser
import Html exposing (Html)
import Html.Events exposing (onInput)
-import Html.Attributes exposing (type_)
+import Html.Attributes exposing (type_, class)
import Bergamot.Syntax exposing (..)
import Bergamot.Search exposing (..)
import Bergamot.Rules exposing (..)
@@ -26,28 +26,40 @@ type Msg
init : Flags -> (Model, Cmd Msg)
init () = ({ program = "", query = "" }, Cmd.none)
-printRules : String -> Maybe String
-printRules progs =
- case run program progs of
- Just prog -> Just (String.join "\n\\quad" (List.map ruleToLatex prog.rules))
- Nothing -> Nothing
+viewSection : String -> Html Msg -> Html Msg
+viewSection name content =
+ Html.div [] [ Html.h2 [] [ Html.text name ], content ]
-proveQuery : String -> String -> Maybe ProofTree
-proveQuery progs querys =
+viewRule : Rule -> Html Msg
+viewRule = latex << ruleToLatex
+
+viewRules : String -> Html Msg
+viewRules progs = viewSection "Rendered Rules" <|
+ Html.div [ class "rule-list" ] <|
+ case run program progs of
+ Just prog -> List.map viewRule prog.rules
+ Nothing -> []
+
+tryProve : String -> String -> Maybe ProofTree
+tryProve progs querys =
case (run program progs, run term querys) of
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
+viewProofTree : String -> String -> Html Msg
+viewProofTree progs querys = viewSection "Proof Tree" <|
+ Html.div [ class "proof-tree" ] <|
+ case tryProve progs querys of
+ Just tree -> [ latex (proofTreeToLatex tree) ]
+ Nothing -> []
+
+
view : Model -> Html Msg
-view m = Html.div []
- [ Html.textarea [ onInput SetProgram ] []
- , Html.br [] []
- , Html.input [ type_ "text", onInput SetQuery ] []
- , latex (Maybe.withDefault "" (printRules m.program))
- , latex (
- proveQuery m.program m.query
- |> Maybe.map proofTreeToLatex
- |> Maybe.withDefault "")
+view m = Html.div [ class "elm-root" ]
+ [ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
+ , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery ] []
+ , viewRules m.program
+ , viewProofTree m.program m.query
]
update : Msg -> Model -> (Model, Cmd Msg)