Put render rules separately from regular rules

This should let us hide them from the user and maybe speed up rendering

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-02 00:25:23 -08:00
parent 1d3f3fd3f8
commit 11dd5ee9fd

View File

@ -39,11 +39,12 @@ modeEq m1 m2 =
type alias Model =
{ program : String
, renderProgram: String
, query : String
, tab : Tab
, editMode : EditMode
}
type alias Flags = { rules: String, query: String }
type alias Flags = { renderRules: String, rules: String, query: String }
type Msg
= SetProgram String
| SetQuery String
@ -51,7 +52,7 @@ type Msg
| SetEditMode EditMode
init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
@ -82,12 +83,12 @@ viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
viewRule env r = renderRuleViaRules env r
|> Maybe.map latex
viewRules : String -> Html Msg
viewRules progs = viewSection "Rendered Rules" <|
viewRules : String -> String -> Html Msg
viewRules renderProgs progs = viewSection "Rendered Rules" <|
Html.div [ class "bergamot-rule-list" ] <|
case run program progs of
Just prog -> List.filterMap (viewRule prog) prog.rules
Nothing -> []
case (run program renderProgs, run program progs) of
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) prog.rules
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal mode querys =
@ -115,7 +116,7 @@ view m = Html.div [ class "bergamot-root" ]
, viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
, viewTab m.tab
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
(Html.Lazy.lazy viewRules m.program)
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewProofTree m.editMode m.program m.query
]