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
            _ -> []

proofGoal : EditMode -> String -> String -> Maybe (Term Metavariable)
proofGoal editMode inputProgs querys =
    case editMode of
        Query -> run term querys
        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] -> Just <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
                                    _ -> Nothing
                            _ -> Nothing
                _ -> Nothing

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

viewProofTree : EditMode -> ResultMode -> String -> String -> String -> String -> Html Msg
viewProofTree editMode resultMode renderProgs inputProgs progs querys =
    Html.div [ class "bergamot-proof-tree" ] <|
        case tryProve editMode inputProgs progs querys of
            Just (MkProofTree tree) ->
                case run program renderProgs of
                    Just renderProg ->
                        let
                            maybeLatexString =
                                case resultMode of
                                    Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion)
                                    Tree -> renderTreeViaRules renderProg (MkProofTree tree)
                        in List.filterMap (Maybe.map latex) [maybeLatexString]
                    Nothing -> []
            Nothing -> []


view : Model -> Html Msg
view m = 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 ] []
        ]
    , viewSection "Result" <| Html.div[]
        [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
        , viewProofTree m.editMode m.resultMode m.renderProgram m.inputProgram m.program m.query
        ]
    , 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 ])
            (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)
        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 )
        ]