160 lines
5.0 KiB
Elm
160 lines
5.0 KiB
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 (..)
|
|
import Json.Encode
|
|
import Maybe
|
|
import Tuple
|
|
|
|
type Tab
|
|
= Editor
|
|
| Rendered
|
|
|
|
tabEq : Tab -> Tab -> Bool
|
|
tabEq t1 t2 =
|
|
case (t1, t2) of
|
|
(Editor, Editor) -> True
|
|
(Rendered, Rendered) -> True
|
|
_ -> False
|
|
|
|
type EditMode
|
|
= Query
|
|
| Syntax
|
|
|
|
modeEq : EditMode -> EditMode -> Bool
|
|
modeEq m1 m2 =
|
|
case (m1, m2) of
|
|
(Query, Query) -> True
|
|
(Syntax, Syntax) -> True
|
|
_ -> False
|
|
|
|
type alias Model =
|
|
{ program : String
|
|
, renderProgram: String
|
|
, query : String
|
|
, tab : Tab
|
|
, editMode : EditMode
|
|
}
|
|
type alias Flags = { renderRules: String, rules: String, query: String }
|
|
type Msg
|
|
= SetProgram String
|
|
| SetQuery String
|
|
| SetTab Tab
|
|
| SetEditMode EditMode
|
|
|
|
init : Flags -> (Model, Cmd Msg)
|
|
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = 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 ]
|
|
|
|
viewTab : Tab -> Html Msg -> Html Msg -> Html Msg
|
|
viewTab tab editor rendered =
|
|
case tab of
|
|
Editor -> editor
|
|
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 modeEq SetEditMode
|
|
|
|
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
|
|
viewRule env r = renderRuleViaRules env r
|
|
|> Maybe.map latex
|
|
|
|
viewRules : String -> String -> Html Msg
|
|
viewRules renderProgs progs = viewSection "Rendered Rules" <|
|
|
Html.div [ class "bergamot-rule-list" ] <|
|
|
case (run program renderProgs, run program progs) of
|
|
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) (List.concatMap .rules prog.sections)
|
|
_ -> []
|
|
|
|
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
|
|
proofGoal mode querys =
|
|
case mode of
|
|
Query -> run term querys
|
|
Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr querys
|
|
|
|
tryProve : EditMode -> String -> String -> Maybe ProofTree
|
|
tryProve mode progs querys =
|
|
case (run program progs, proofGoal mode querys) of
|
|
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
|
|
_ -> Nothing
|
|
|
|
viewProofTree : EditMode -> String -> String -> Html Msg
|
|
viewProofTree mode progs querys = viewSection "Proof Tree" <|
|
|
Html.div [ class "bergamot-proof-tree" ] <|
|
|
case tryProve mode 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")]
|
|
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
|
, viewTab m.tab
|
|
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
|
|
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
|
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
|
|
, viewProofTree m.editMode 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)
|
|
SetEditMode mode -> ({ m | editMode = 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 )
|
|
]
|