bergamot-elm/src/Main.elm

99 lines
2.8 KiB
Elm
Raw Normal View History

2023-11-26 11:43:38 -08:00
module Main exposing (main)
import Browser
import Html exposing (Html)
2023-11-26 11:58:20 -08:00
import Html.Events exposing (onInput)
import Html.Attributes exposing (type_, class, value)
2023-11-26 11:43:38 -08:00
import Bergamot.Syntax exposing (..)
import Bergamot.Search exposing (..)
import Bergamot.Rules exposing (..)
import Bergamot.Parser exposing (..)
2023-11-26 14:34:52 -08:00
import Bergamot.Latex exposing (..)
2023-11-26 15:54:01 -08:00
import Json.Encode
2023-11-26 11:43:38 -08:00
import Maybe
import Tuple
import Debug
type alias Model =
{ program : String
, query : String
}
type alias Flags = { rules: String, query: String }
2023-11-26 11:58:20 -08:00
type Msg
= SetProgram String
| SetQuery String
2023-11-26 11:43:38 -08:00
init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, query = fs.query }, 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 ]
2023-11-26 14:34:52 -08:00
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
2023-11-26 11:43:38 -08:00
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 -> []
2023-11-26 11:43:38 -08:00
view : Model -> Html Msg
view m = Html.div [ class "bergamot-root" ]
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewRules m.program
, viewProofTree m.program m.query
2023-11-26 11:58:20 -08:00
]
2023-11-26 11:43:38 -08:00
update : Msg -> Model -> (Model, Cmd Msg)
update msg m =
case msg of
2023-11-26 11:58:20 -08:00
SetProgram prog -> ({ m | program = prog }, Cmd.none)
SetQuery query -> ({ m | query = query }, Cmd.none)
2023-11-26 11:43:38 -08:00
subscriptions : Model -> Sub Msg
subscriptions _ = Sub.none
main =
Browser.element
{ init = init
, view = view
, update = update
, subscriptions = subscriptions
}
2023-11-26 15:54:01 -08:00
-- 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 )
]