From 9fd60b4013a733eadebcc45d8579cd967e04bea7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 22 Dec 2023 15:22:46 -0800 Subject: [PATCH] Reorganize the UI somewhat and add conclusion-only view Signed-off-by: Danila Fedorin --- src/Main.elm | 77 +++++++++++++++++++++++++++++++++++----------------- 1 file changed, 52 insertions(+), 25 deletions(-) diff --git a/src/Main.elm b/src/Main.elm index f9342dd..c17209a 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -33,19 +33,31 @@ type EditMode = Query | Syntax -modeEq : EditMode -> EditMode -> Bool -modeEq m1 m2 = +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 - , query : String , tab : Tab + , query : String , editMode : EditMode + , resultMode : ResultMode } type alias Flags = { renderRules: String, rules: String, query: String } type Msg @@ -54,9 +66,10 @@ type Msg | SetQuery String | SetTab Tab | SetEditMode EditMode + | SetResultMode ResultMode init : Flags -> (Model, Cmd Msg) -init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none) +init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none) viewSection : String -> Html Msg -> Html Msg viewSection name content = @@ -82,7 +95,10 @@ viewTabSelector : Tab -> List (Tab, String) -> Html Msg viewTabSelector = viewSelector tabEq SetTab viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg -viewEditModeSelector = viewSelector modeEq SetEditMode +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 @@ -99,48 +115,58 @@ viewRuleSection env sec = ]) viewRules : String -> String -> Html Msg -viewRules renderProgs progs = viewSection "Rendered Rules" <| +viewRules renderProgs progs = Html.div [ class "bergamot-section-list" ] <| case (run program renderProgs, run program progs) of (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections _ -> [] proofGoal : EditMode -> String -> Maybe (Term Metavariable) -proofGoal mode querys = - case mode of +proofGoal editMode querys = + case editMode of Query -> run term querys Syntax -> Maybe.map (\e -> Call "type" [Call "empty" [], 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 +tryProve editMode progs querys = + case (run program progs, proofGoal editMode querys) of (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) _ -> Nothing -viewProofTree : EditMode -> String -> String -> String -> Html Msg -viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <| +viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg +viewProofTree editMode resultMode renderProgs progs querys = Html.div [ class "bergamot-proof-tree" ] <| - case tryProve mode progs querys of - Just tree -> + case tryProve editMode progs querys of + Just (MkProofTree tree) -> case run program renderProgs of Just renderProg -> - List.map latex - <| List.filterMap (renderTreeViaRules renderProg) - <| [ tree ] + let + maybeLatexString = + case resultMode of + Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion) + Tree -> renderTreeViaRules renderProg (MkProofTree tree) + in List.filterMap (Maybe.map latex) [maybeLatexString] Nothing -> [] Nothing -> [] view : Model -> Html Msg view m = Html.div [ class "bergamot-root" ] - [ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta Rule Editor"), (Rendered, "Rendered Rules")] - , viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")] - , viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] [] - , viewProofTree m.editMode m.renderProgram m.program m.query - , viewTab m.tab - (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]) - (viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ]) - (Html.Lazy.lazy2 viewRules m.renderProgram m.program) + [ viewSection "Input" <| Html.div [] + [ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")] + , Html.input [ type_ "text", onInput SetQuery, value m.query ] [] + ] + , viewSection "Result" <| Html.div[] + [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")] + , viewProofTree m.editMode m.resultMode m.renderProgram m.program m.query + ] + , viewSection "Rules" <| Html.div [] + [ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")] + , viewTab m.tab + (Html.textarea [ onInput SetProgram ] [ Html.text m.program ]) + (Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ]) + (Html.Lazy.lazy2 viewRules m.renderProgram m.program) + ] ] update : Msg -> Model -> (Model, Cmd Msg) @@ -151,6 +177,7 @@ update msg m = 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