Switch entirely to using rules to render rules.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
84c79ddb50
commit
363e52ec5e
|
@ -22,51 +22,45 @@ renderTermViaRules env t =
|
||||||
Call "latex" [_, StringLit s] -> Just s
|
Call "latex" [_, StringLit s] -> Just s
|
||||||
_ -> Nothing)
|
_ -> Nothing)
|
||||||
|
|
||||||
renderRuleViaRules : RuleEnv -> Rule -> Maybe String
|
buildInferenceRuleFrac : List String -> String -> String -> String
|
||||||
renderRuleViaRules env r =
|
buildInferenceRuleFrac prems conc name = String.concat
|
||||||
let
|
|
||||||
quotedPrems = List.map (Syntax.andThen quoteMetavariable) r.premises
|
|
||||||
quotedConc = Syntax.andThen quoteMetavariable r.conclusion
|
|
||||||
buildStr conc prems = String.concat
|
|
||||||
[ "\\cfrac{"
|
[ "\\cfrac{"
|
||||||
, String.join "\\quad " prems
|
, String.join "\\quad " prems
|
||||||
, "}{"
|
, "}{"
|
||||||
, conc
|
, conc
|
||||||
, "}\\ \\texttt{"
|
, "}\\ \\texttt{"
|
||||||
, r.name
|
, name
|
||||||
, "}"
|
, "}"
|
||||||
]
|
]
|
||||||
|
|
||||||
|
renderRuleViaRules : RuleEnv -> Rule -> Maybe String
|
||||||
|
renderRuleViaRules env r =
|
||||||
|
let
|
||||||
|
quotedPrems = List.map quoteMetavariables r.premises
|
||||||
|
quotedConc = quoteMetavariables r.conclusion
|
||||||
in
|
in
|
||||||
renderTermViaRules env quotedConc
|
renderTermViaRules env quotedConc
|
||||||
|> Maybe.andThen (\conc ->
|
|> Maybe.andThen (\conc ->
|
||||||
sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
|
sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
|
||||||
|> Maybe.map (\prems -> buildStr conc prems))
|
|> Maybe.map (\prems -> buildInferenceRuleFrac prems conc r.name))
|
||||||
|
|
||||||
quoteMetavariable : Metavariable -> Term Void
|
renderTreeViaRules : RuleEnv -> ProofTree -> Maybe String
|
||||||
quoteMetavariable v = Call "metavariable" [StringLit <| metavariableToLatex v]
|
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
|
quote : String -> (a -> String) -> Term a -> Term Void
|
||||||
termToLatex f t =
|
quote s f =
|
||||||
case t of
|
let helper a = Call s [StringLit <| f a]
|
||||||
Call "intlit" [t1] -> termToLatex f t1
|
in Syntax.andThen helper
|
||||||
Call "strlit" [t1] -> termToLatex f t1
|
|
||||||
Call "var" [t1] -> termToLatex f t1
|
quoteMetavariables : Term Metavariable -> Term Void
|
||||||
Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
|
quoteMetavariables = quote "metavariable" metavariableToLatex
|
||||||
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
|
quoteVariables : Term UnificationVar -> Term Void
|
||||||
Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
|
quoteVariables = quote "variable" (\(MkUnificationVar v) -> v)
|
||||||
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) ++ "\"" ++ "}"
|
|
||||||
|
|
||||||
metavariableToLatex : Metavariable -> String
|
metavariableToLatex : Metavariable -> String
|
||||||
metavariableToLatex (MkMetavariable s) =
|
metavariableToLatex (MkMetavariable s) =
|
||||||
|
@ -75,12 +69,3 @@ metavariableToLatex (MkMetavariable s) =
|
||||||
in
|
in
|
||||||
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
|
if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
|
||||||
if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
|
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 ++ "}"
|
|
||||||
|
|
14
src/Main.elm
14
src/Main.elm
|
@ -113,11 +113,17 @@ tryProve mode progs querys =
|
||||||
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
|
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
|
|
||||||
viewProofTree : EditMode -> String -> String -> Html Msg
|
viewProofTree : EditMode -> String -> String -> String -> Html Msg
|
||||||
viewProofTree mode progs querys = viewSection "Proof Tree" <|
|
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
|
||||||
Html.div [ class "bergamot-proof-tree" ] <|
|
Html.div [ class "bergamot-proof-tree" ] <|
|
||||||
case tryProve mode progs querys of
|
case tryProve mode progs querys of
|
||||||
Just tree -> [ latex (proofTreeToLatex tree) ]
|
Just tree ->
|
||||||
|
case run program renderProgs of
|
||||||
|
Just renderProg ->
|
||||||
|
List.map latex
|
||||||
|
<| List.filterMap (renderTreeViaRules renderProg)
|
||||||
|
<| [ tree ]
|
||||||
|
Nothing -> []
|
||||||
Nothing -> []
|
Nothing -> []
|
||||||
|
|
||||||
|
|
||||||
|
@ -126,7 +132,7 @@ view m = Html.div [ class "bergamot-root" ]
|
||||||
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
|
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (Rendered, "Rendered Rules")]
|
||||||
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
|
||||||
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
|
, 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
|
, viewTab m.tab
|
||||||
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
|
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
|
||||||
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user