bergamot-elm/src/Main.elm

module Main exposing (main)

import Browser
import Html exposing (Html)
import Html.Events exposing (onInput, onClick)
import Html.Attributes exposing (type_, class, classList, value)
import Bergamot.Syntax exposing (..)
import Bergamot.Search exposing (..)
import Bergamot.Rules exposing (..)
import Bergamot.Parser exposing (..)
import Bergamot.Latex exposing (..)
import Json.Encode
import Maybe
import Tuple
import Debug

type Tab
    = Editor
    | Rendered

tabEq : Tab -> Tab -> Bool
tabEq t1 t2 =
    case (t1, t2) of
        (Editor, Editor) -> True
        (Rendered, Rendered) -> True
        _ -> False

type alias Model =
    { program : String
    , query : String
    , tab: Tab
    }
type alias Flags = { rules: String, query: String }
type Msg
    = SetProgram String
    | SetQuery String
    | SetTab Tab

init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, query = fs.query, tab = Editor }, Cmd.none)

viewSection : String -> Html Msg -> Html Msg
viewSection name content =
    Html.div [ class "bergamot-section" ] [ Html.em [ class "bergamot-section-heading" ] [ Html.text name ], content ]

viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
viewTab tab editor rendered =
    case tab of
        Editor -> editor
        Rendered -> rendered

viewTabSelector : Tab -> List (Tab, String) -> Html Msg
viewTabSelector tab tabNames = Html.div [ class "bergamot-tab-selector" ] <|
    List.map (\(tabp, name) ->
        Html.button
            [ classList [("active", tabEq tab tabp)]
            , onClick (SetTab tabp)
            ] [ Html.text name ]) tabNames

viewRule : Rule -> Html Msg
viewRule = latex << ruleToLatex

viewRules : String -> Html Msg
viewRules progs = viewSection "Rendered Rules" <|
    Html.div [ class "bergamot-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 "bergamot-proof-tree" ] <|
      case tryProve progs querys of
          Just tree -> [ latex (proofTreeToLatex tree) ]
          Nothing -> []


view : Model -> Html Msg
view m = Html.div [ class "bergamot-root" ]
    [ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
    , viewTab m.tab
        (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
        (viewRules m.program)
    , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
    , viewProofTree m.program m.query
    ]

update : Msg -> Model -> (Model, Cmd Msg)
update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
        SetQuery query -> ({ m | query = query }, Cmd.none)
        SetTab tab -> ({ m | tab = tab }, Cmd.none)

subscriptions : Model -> Sub Msg
subscriptions _ = Sub.none

main =
    Browser.element
        { init = init
        , view = view
        , update = update
        , subscriptions = subscriptions
        }

-- Latex support:
-- Based on https://stackoverflow.com/questions/75492820/embedding-mathematical-equations-in-an-elm-spa

latex : String -> Html Msg
latex expr =
  Html.node "katex-expression"
    [ Html.Attributes.attribute "expression" expr
    , Html.Attributes.attribute "katex-options" (Json.Encode.encode 0 options)
    ]
    []


options : Json.Encode.Value
options =
    Json.Encode.object
        [ ( "displayMode", Json.Encode.bool True )
        ]