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 Html.Lazy
import Bergamot.Syntax exposing (..)
import Bergamot.Search exposing (..)
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

type Tab
    = Editor
    | Rendered

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

type EditMode
    = Query
    | Syntax

modeEq : EditMode -> EditMode -> Bool
modeEq m1 m2 =
    case (m1, m2) of
        (Query, Query) -> True
        (Syntax, Syntax) -> True
        _ -> False

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

init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, 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

viewSelector : (a -> a -> Bool) -> (a -> Msg) -> a -> List (a, String) -> Html Msg
viewSelector eq mkMsg mode modeNames =
    Html.div [ class "bergamot-selector" ] <|
        List.map (\(modep, name) ->
            Html.button
                [ classList [("active", eq mode modep)]
                , onClick (mkMsg modep)
                ] [ Html.text name ]) modeNames

viewTabSelector : Tab -> List (Tab, String) -> Html Msg
viewTabSelector = viewSelector tabEq SetTab

viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
viewEditModeSelector = viewSelector modeEq SetEditMode

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-section-list" ] <|
        case (run program renderProgs, run program progs) of
            (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" [Call "empty" [], exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys

tryProve : EditMode -> String -> String -> Maybe ProofTree
tryProve mode progs querys =
    case (run program progs, proofGoal mode querys) of
        (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
        _ -> Nothing

viewProofTree : EditMode -> String -> String -> String -> Html Msg
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
    Html.div [ class "bergamot-proof-tree" ] <|
        case tryProve mode progs querys of
            Just tree ->
                case run program renderProgs of
                    Just renderProg ->
                        List.map latex
                            <| List.filterMap (renderTreeViaRules renderProg)
                            <| [ tree ]
                    Nothing -> []
            Nothing -> []


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.renderProgram 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)
    ]

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)
        SetEditMode mode -> ({ m | editMode = mode }, 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 )
        ]