bergamot-elm/src/Main.elm

module Main exposing (main)

import Browser
import Html exposing (Html)
import Html.Events exposing (onInput)
import Html.Attributes exposing (type_)
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 alias Model =
    { program : String
    , query : String
    }
type alias Flags = ()
type Msg
    = SetProgram String
    | SetQuery String

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

proveQuery : String -> String -> Maybe ProofTree
proveQuery progs querys =
    case (run program progs, run term querys) of
        (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
        _ -> 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 "")
    ]

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)

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