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 (topLevelExpr, exprToTerm)
import Bergamot.Utils exposing (..)
import Json.Encode
import Maybe
import Tuple

type Tab
    = Editor
    | MetaEditor
    | Rendered

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

type EditMode
    = Query
    | Syntax

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

type ResultMode
    = Conclusion
    | Tree

resultModeEq : ResultMode -> ResultMode -> Bool
resultModeEq rm1 rm2 =
    case (rm1, rm2) of
        (Conclusion, Conclusion) -> True
        (Tree, Tree) -> True
        _ -> False

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

init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, inputProgram = fs.inputRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, 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 -> Html Msg
viewTab tab editor metaEditor rendered =
    case tab of
        Editor -> editor
        MetaEditor -> metaEditor
        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 editModeEq SetEditMode

viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
viewResultModeSelector = viewSelector resultModeEq SetResultMode

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 =
    Html.div [ class "bergamot-section-list" ] <|
        case (run program renderProgs, run program progs) of
            (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
            _ -> []

type Error
    = BadQuery
    | BadObjectTerm
    | NoConversionResults
    | BadInputProg
    | BadProg
    | BadRenderProg
    | FailedRender
    | Silent

combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
combineTwoResults f ra rb =
    case ra of
        Err _ -> Err Silent
        Ok a ->
            case rb of
                Err _ -> Err Silent
                Ok b -> f a b

errorToString : Error -> String
errorToString err =
    case err of
        BadQuery -> "Unable to parse input query"
        BadObjectTerm -> "Unable to parse input object language term"
        NoConversionResults -> "Failed to convert object language term to proof goal"
        BadInputProg -> "Unable to parse conversion rules from object language to proof goals"
        BadProg -> "Unable to parse rules"
        BadRenderProg -> "Unable to parse rendering rules"
        FailedRender -> "Unable to render terms using provided rendering rules"
        Silent -> ""

viewError : Error -> Html Msg
viewError e = Html.div [ class "bergamot-error" ] [ Html.text <| errorToString e ]

viewIfError : Result Error a -> List (Html Msg)
viewIfError r =
    case r of
        Err Silent -> []
        Err e -> [ viewError e ]
        _ -> []

viewOrError : Result Error (Html Msg) -> Html Msg
viewOrError r =
    case r of
        Err Silent -> Html.div [] []
        Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
        Ok html -> html

proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable)
proofGoal editMode inputProgs querys =
    if querys == ""
    then Err Silent
    else
        case editMode of
            Query ->
                case run topLevelTerm querys of
                    Nothing -> Err BadQuery
                    Just query -> Ok query
            Syntax ->
                case (run program inputProgs, run topLevelExpr querys) of
                    (Just inputProg, Just e) ->
                        let
                            inputRule = { name = "UserInput", premises = [], conclusion = Call "input" [exprToTerm e] }
                            fullProgram = { sections = { name = "", rules = [inputRule] } :: inputProg.sections }
                            query = Call "prompt" [Var (MkMetavariable "?p")]
                        in
                            case single fullProgram (prove query |> Bergamot.Rules.andThen reifyProofTree) of
                                Just (MkProofTree node) ->
                                    case node.conclusion of
                                        Call "prompt" [t] -> Ok <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
                                        _ -> Err NoConversionResults
                                _ -> Err NoConversionResults
                    (_, Nothing) -> Err BadObjectTerm
                    (Nothing, _) -> Err BadInputProg

progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
progAndRenderProg progs renderProgs =
    case (run program progs, run program renderProgs) of
        (Just prog, Just renderProg) -> Ok (prog, renderProg)
        (Nothing, _) -> Err BadProg
        (_, Nothing) -> Err BadRenderProg

renderProofTree : ResultMode -> ProofTree -> RuleEnv -> Result Error (Html Msg)
renderProofTree resultMode (MkProofTree node) renderProg =
    let
        maybeLatexString =
            case resultMode of
                Conclusion -> renderTermViaRules renderProg (quoteVariables node.conclusion)
                Tree -> renderTreeViaRules renderProg (MkProofTree node)
    in
        List.filterMap (Maybe.map latex) [maybeLatexString]
        |> Html.div [ class "bergamot-proof-tree" ]
        |> Ok


viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result Error (Html Msg)
viewProofTree resultMode query (prog, renderProg) =
    case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
        Just proofTree -> renderProofTree resultMode proofTree renderProg
        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ] []

view : Model -> Html Msg
view m =
    let
        termOrErr = proofGoal m.editMode m.inputProgram m.query
        progsOrErr = progAndRenderProg m.program m.renderProgram
        proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
    in
        Html.div [ class "bergamot-root" ]
        [ viewSection "Input" <| Html.div [] <|
            [ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
            , Html.input [ type_ "text", onInput SetQuery, value m.query ] []
            ] ++
            viewIfError termOrErr
        , viewSection "Result" <| Html.div[]
            [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
            , viewOrError proofTreeOrErr
            ]
        , viewSection "Rules" <| Html.div [] <|
            [ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
            , viewTab m.tab
                (Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
                (Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
                (viewRules m.renderProgram m.program)
            ] ++
            viewIfError progsOrErr
        ]

update : Msg -> Model -> (Model, Cmd Msg)
update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
        SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
        SetQuery query -> ({ m | query = query }, Cmd.none)
        SetTab tab -> ({ m | tab = tab }, Cmd.none)
        SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
        SetResultMode mode -> ({ m | resultMode = 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 )
        ]