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 Bergamot.ObjectLanguage 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 ] []
    , Html.text (Debug.toString <| run parseExpr 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 )
        ]