From 10d1edbc3279871fe1df51009ec7c055e9c7b416 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 25 Dec 2023 13:42:20 -0800 Subject: [PATCH] Add error reporting Signed-off-by: Danila Fedorin --- src/Bergamot/Parser.elm | 3 + src/Main.elm | 176 +++++++++++++++++++++++++++------------- 2 files changed, 124 insertions(+), 55 deletions(-) diff --git a/src/Bergamot/Parser.elm b/src/Bergamot/Parser.elm index 2d6f20c..01467ab 100644 --- a/src/Bergamot/Parser.elm +++ b/src/Bergamot/Parser.elm @@ -82,6 +82,9 @@ term = Parser.lazy (\() -> Parser.oneOf , Parser.succeed StringLit |= strLit ]) +topLevelTerm : Parser (Term Metavariable) +topLevelTerm = term |. Parser.end + rule : Parser Rule rule = let diff --git a/src/Main.elm b/src/Main.elm index c5ff95b..93536a5 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -122,67 +122,133 @@ viewRules renderProgs progs = (Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections _ -> [] -proofGoal : EditMode -> String -> String -> Maybe (Term Metavariable) +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 = - case editMode of - Query -> run term querys - 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] -> Just <| Bergamot.Syntax.map (MkMetavariable << unUnificationVar) t - _ -> Nothing - _ -> Nothing - _ -> Nothing - -tryProve : EditMode -> String -> String -> String -> Maybe ProofTree -tryProve editMode inputProgs progs querys = - case (run program progs, proofGoal editMode inputProgs querys) of - (Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) - _ -> Nothing - -viewProofTree : EditMode -> ResultMode -> String -> String -> String -> String -> Html Msg -viewProofTree editMode resultMode renderProgs inputProgs progs querys = - Html.div [ class "bergamot-proof-tree" ] <| - case tryProve editMode inputProgs progs querys of - Just (MkProofTree tree) -> - case run program renderProgs of - Just renderProg -> + 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 - maybeLatexString = - case resultMode of - Conclusion -> renderTermViaRules renderProg (quoteVariables tree.conclusion) - Tree -> renderTreeViaRules renderProg (MkProofTree tree) - in List.filterMap (Maybe.map latex) [maybeLatexString] - Nothing -> [] - Nothing -> [] + 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 = 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 ] [] +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 ] [ Html.text m.program ]) + (Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ]) + (viewRules m.renderProgram m.program) + ] ++ + viewIfError progsOrErr ] - , viewSection "Result" <| Html.div[] - [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")] - , viewProofTree m.editMode m.resultMode m.renderProgram m.inputProgram 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) update msg m =