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 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 ] []
    , Html.pre [] [ Html.code [] [ Html.text (Maybe.withDefault "" (printRules m.program)) ] ]
    , Html.pre [] [ Html.code [] [ Html.text (
        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
        }