Everything-I-Know-About-Types/bergamot-elm
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Render sections in widget

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-21 14:06:37 -08:00
parent 678e51f146
commit 84c79ddb50
1 changed files with 16 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
src/Main.elm
View File

@ -11,6 +11,7 @@ import Bergamot.Rules exposing (..)
import Bergamot.Parser exposing (..)
import Bergamot.Latex exposing (..)
import Bergamot.ObjectLanguage exposing (..)
import Bergamot.Utils exposing (..)
import Json.Encode
import Maybe
import Tuple
@ -83,18 +84,28 @@ viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
viewRule env r = renderRuleViaRules env r
|> Maybe.map latex
viewRuleSection : RuleEnv -> Section -> Maybe (Html Msg)
viewRuleSection env sec =
List.map (viewRule env) sec.rules
|> sequenceMaybes
|> Maybe.map (\rs ->
Html.div [ class "bergamot-rule-section" ]
[ Html.div [ class "bergamot-rule-list" ] rs
, Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
])
viewRules : String -> String -> Html Msg
viewRules renderProgs progs = viewSection "Rendered Rules" <|
Html.div [ class "bergamot-rule-list" ] <|
Html.div [ class "bergamot-section-list" ] <|
case (run program renderProgs, run program progs) of
(Just renderProg, Just prog) -> List.filterMap (viewRule renderProg) (List.concatMap .rules prog.sections)
(Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal mode querys =
case mode of
Query -> run term querys
Syntax -> Maybe.map (\e -> Call "type" [exprToTerm e, Var (MkMetavariable "tau")]) <| run parseExpr 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 =
@ -114,11 +125,11 @@ view : Model -> Html Msg
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
, viewTab m.tab
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text 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
]
update : Msg -> Model -> (Model, Cmd Msg)