291 lines
10 KiB
Elm
291 lines
10 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 (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 progAndRenderProg progs renderProgs of
|
|
Ok (prog, renderProg) -> List.filterMap (viewRuleSection renderProg) prog.sections
|
|
_ -> []
|
|
|
|
type Error
|
|
= BadQuery
|
|
| BadObjectTerm
|
|
| NoConversionResults
|
|
| BadInputProg
|
|
| BadProg
|
|
| BadRenderProg
|
|
| FailedRender
|
|
| Silent
|
|
|
|
combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
|
|
combineTwoResults f ra rb =
|
|
case ra of
|
|
Err _ -> Err Silent
|
|
Ok a ->
|
|
case rb of
|
|
Err _ -> Err Silent
|
|
Ok b -> f a b
|
|
|
|
errorToString : Error -> String
|
|
errorToString err =
|
|
case err of
|
|
BadQuery -> "Unable to parse input query"
|
|
BadObjectTerm -> "Unable to parse input object language term"
|
|
NoConversionResults -> "Failed to convert object language term to proof goal"
|
|
BadInputProg -> "Unable to parse conversion rules from object language to proof goals"
|
|
BadProg -> "Unable to parse rules"
|
|
BadRenderProg -> "Unable to parse rendering rules"
|
|
FailedRender -> "Unable to render terms using provided rendering rules"
|
|
Silent -> ""
|
|
|
|
viewError : Error -> Html Msg
|
|
viewError e = Html.div [ class "bergamot-error" ] [ Html.text <| errorToString e ]
|
|
|
|
viewIfError : Result Error a -> List (Html Msg)
|
|
viewIfError r =
|
|
case r of
|
|
Err Silent -> []
|
|
Err e -> [ viewError e ]
|
|
_ -> []
|
|
|
|
viewOrError : Result Error (Html Msg) -> Html Msg
|
|
viewOrError r =
|
|
case r of
|
|
Err Silent -> Html.div [] []
|
|
Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
|
|
Ok html -> html
|
|
|
|
proofGoal : EditMode -> String -> String -> Result Error (Term Metavariable)
|
|
proofGoal editMode inputProgs querys =
|
|
if querys == ""
|
|
then Err Silent
|
|
else
|
|
case editMode of
|
|
Query ->
|
|
case run topLevelTerm querys of
|
|
Nothing -> Err BadQuery
|
|
Just query -> Ok query
|
|
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] -> Ok <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t
|
|
_ -> Err NoConversionResults
|
|
_ -> Err NoConversionResults
|
|
(_, Nothing) -> Err BadObjectTerm
|
|
(Nothing, _) -> Err BadInputProg
|
|
|
|
progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
|
|
progAndRenderProg progs renderProgs =
|
|
case (run program progs, run program renderProgs) of
|
|
(Just prog, Just renderProg) -> Ok (prog, renderProg)
|
|
(Nothing, _) -> Err BadProg
|
|
(_, Nothing) -> Err BadRenderProg
|
|
|
|
renderProofTree : ResultMode -> ProofTree -> RuleEnv -> Result Error (Html Msg)
|
|
renderProofTree resultMode (MkProofTree node) renderProg =
|
|
let
|
|
maybeLatexString =
|
|
case resultMode of
|
|
Conclusion -> renderTermViaRules renderProg (quoteVariables node.conclusion)
|
|
Tree -> renderTreeViaRules renderProg (MkProofTree node)
|
|
in
|
|
List.filterMap (Maybe.map latex) [maybeLatexString]
|
|
|> Html.div [ class "bergamot-proof-tree" ]
|
|
|> Ok
|
|
|
|
|
|
viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result Error (Html Msg)
|
|
viewProofTree resultMode query (prog, renderProg) =
|
|
case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
|
|
Just proofTree -> renderProofTree resultMode proofTree renderProg
|
|
Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ] []
|
|
|
|
view : Model -> Html Msg
|
|
view m =
|
|
let
|
|
termOrErr = proofGoal m.editMode m.inputProgram m.query
|
|
progsOrErr = progAndRenderProg m.program m.renderProgram
|
|
proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
|
|
in
|
|
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 ] []
|
|
] ++
|
|
viewIfError termOrErr
|
|
, viewSection "Result" <| Html.div[]
|
|
[ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
|
|
, viewOrError proofTreeOrErr
|
|
]
|
|
, viewSection "Rules" <| Html.div [] <|
|
|
[ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
|
|
, viewTab m.tab
|
|
(Html.textarea [ onInput SetProgram, value m.program ] [ ])
|
|
(Html.textarea [ onInput SetRenderProgram, value m.renderProgram ] [ ])
|
|
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
|
] ++
|
|
viewIfError progsOrErr
|
|
]
|
|
|
|
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 )
|
|
]
|