From 363e52ec5e3b24afe99801194659b7b4f2f43baf Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 21 Dec 2023 14:45:04 -0800 Subject: [PATCH] Switch entirely to using rules to render rules. Signed-off-by: Danila Fedorin --- src/Bergamot/Latex.elm | 75 +++++++++++++++++------------------------- src/Main.elm | 18 ++++++---- 2 files changed, 42 insertions(+), 51 deletions(-) diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm index dec8b07..683f1cb 100644 --- a/src/Bergamot/Latex.elm +++ b/src/Bergamot/Latex.elm @@ -22,51 +22,45 @@ renderTermViaRules env t = Call "latex" [_, StringLit s] -> Just s _ -> Nothing) +buildInferenceRuleFrac : List String -> String -> String -> String +buildInferenceRuleFrac prems conc name = String.concat + [ "\\cfrac{" + , String.join "\\quad " prems + , "}{" + , conc + , "}\\ \\texttt{" + , name + , "}" + ] + renderRuleViaRules : RuleEnv -> Rule -> Maybe String renderRuleViaRules env r = let - quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises - quotedConc = Syntax.andThen quoteMetavariable r.conclusion - buildStr conc prems = String.concat - [ "\\cfrac{" - , String.join "\\quad " prems - , "}{" - , conc - , "}\\ \\texttt{" - , r.name - , "}" - ] + quotedPrems = List.map quoteMetavariables r.premises + quotedConc = quoteMetavariables r.conclusion in renderTermViaRules env quotedConc |> Maybe.andThen (\conc -> sequenceMaybes (List.map (renderTermViaRules env) quotedPrems) - |> Maybe.map (\prems -> buildStr conc prems)) + |> Maybe.map (\prems -> buildInferenceRuleFrac prems conc r.name)) -quoteMetavariable : Metavariable -> Term Void -quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v] +renderTreeViaRules : RuleEnv -> ProofTree -> Maybe String +renderTreeViaRules env (MkProofTree node) = + renderTermViaRules env (quoteVariables node.conclusion) + |> Maybe.andThen (\conc -> + sequenceMaybes (List.map (renderTreeViaRules env) node.premises) + |> Maybe.map (\prems -> buildInferenceRuleFrac prems conc node.name)) -termToLatex : (a -> String) -> Term a -> String -termToLatex f t = - case t of - Call "intlit" [t1] -> termToLatex f t1 - Call "strlit" [t1] -> termToLatex f t1 - Call "var" [t1] -> termToLatex f t1 - Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2 - Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")" - Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3 - Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2 - Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 - Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3 - Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2 - Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2 - Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3 - Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3 - Call "empty" [] -> "\\varnothing" - Call s [] -> "\\text{" ++ s ++ "}" - Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")" - Var x -> f x - IntLit i -> String.fromInt i - StringLit s -> "\\texttt{" ++ "\"" ++ encodeLatex (encodeStr s) ++ "\"" ++ "}" +quote : String -> (a -> String) -> Term a -> Term Void +quote s f = + let helper a = Call s [StringLit <| f a] + in Syntax.andThen helper + +quoteMetavariables : Term Metavariable -> Term Void +quoteMetavariables = quote "metavariable" metavariableToLatex + +quoteVariables : Term UnificationVar -> Term Void +quoteVariables = quote "variable" (\(MkUnificationVar v) -> v) metavariableToLatex : Metavariable -> String metavariableToLatex (MkMetavariable s) = @@ -75,12 +69,3 @@ metavariableToLatex (MkMetavariable s) = in if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion - -ruleToLatex : Rule -> String -ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}" - -unificationVarToLatex : UnificationVar -> String -unificationVarToLatex (MkUnificationVar s) = s - -proofTreeToLatex : ProofTree -> String -proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}" diff --git a/src/Main.elm b/src/Main.elm index 458eef7..764a369 100644 --- a/src/Main.elm +++ b/src/Main.elm @@ -113,12 +113,18 @@ tryProve mode progs querys = (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" <| +viewProofTree : EditMode -> String -> String -> String -> Html Msg +viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <| Html.div [ class "bergamot-proof-tree" ] <| - case tryProve mode progs querys of - Just tree -> [ latex (proofTreeToLatex tree) ] - Nothing -> [] + case tryProve mode progs querys of + Just tree -> + case run program renderProgs of + Just renderProg -> + List.map latex + <| List.filterMap (renderTreeViaRules renderProg) + <| [ tree ] + Nothing -> [] + Nothing -> [] view : Model -> Html Msg @@ -126,7 +132,7 @@ view m = Html.div [ class "bergamot-root" ] [ viewTabSelector m.tab [(Editor, "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.program m.query + , viewProofTree m.editMode m.renderProgram m.program m.query , viewTab m.tab (viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]) (Html.Lazy.lazy2 viewRules m.renderProgram m.program)