From 33c3f87564f9f43f0f310923b14ac1caa524d0e7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 26 Nov 2023 16:25:23 -0800 Subject: [PATCH] Add some styling (still very early stages) --- index.html | 35 +++++++++++++++++++++++++++++++++++ src/Main.elm | 46 +++++++++++++++++++++++++++++----------------- 2 files changed, 64 insertions(+), 17 deletions(-) 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)