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

Reorganize the UI somewhat and add conclusion-only view

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-12-22 15:22:46 -08:00
parent aa7fd44a6d
commit 9fd60b4013
1 changed files with 52 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

77
src/Main.elm
View File

@ -33,19 +33,31 @@ type EditMode
= Query
| Syntax
modeEq : EditMode -> EditMode -> Bool
modeEq m1 m2 =
editModeEq : EditMode -> EditMode -> Bool
editModeEq m1 m2 =
case (m1, m2) of
(Query, Query) -> True
(Syntax, Syntax) -> True
_ -> False
type ResultMode
= Conclusion
| Tree
resultModeEq : ResultMode -> ResultMode -> Bool
resultModeEq rm1 rm2 =
case (rm1, rm2) of
(Conclusion, Conclusion) -> True
(Tree, Tree) -> True
_ -> False
type alias Model =
{ program : String
, renderProgram: String
, query : String
, tab : Tab
, query : String
, editMode : EditMode
, resultMode : ResultMode
}
type alias Flags = { renderRules: String, rules: String, query: String }
type Msg
@ -54,9 +66,10 @@ type Msg
| SetQuery String
| SetTab Tab
| SetEditMode EditMode
| SetResultMode ResultMode
init : Flags -> (Model, Cmd Msg)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Editor, editMode = Query }, Cmd.none)
init fs = ({ program = fs.rules, renderProgram = fs.renderRules, query = fs.query, tab = Rendered, editMode = Syntax, resultMode = Conclusion }, Cmd.none)
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
@ -82,7 +95,10 @@ viewTabSelector : Tab -> List (Tab, String) -> Html Msg
viewTabSelector = viewSelector tabEq SetTab
viewEditModeSelector : EditMode -> List (EditMode, String) -> Html Msg
viewEditModeSelector = viewSelector modeEq SetEditMode
viewEditModeSelector = viewSelector editModeEq SetEditMode
viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
viewResultModeSelector = viewSelector resultModeEq SetResultMode
viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
viewRule env r = renderRuleViaRules env r
@ -99,48 +115,58 @@ viewRuleSection env sec =
])
viewRules : String -> String -> Html Msg
viewRules renderProgs progs = viewSection "Rendered Rules" <|
viewRules renderProgs progs =
Html.div [ class "bergamot-section-list" ] <|
case (run program renderProgs, run program progs) of
(Just renderProg, Just prog) -> List.filterMap (viewRuleSection renderProg) prog.sections
_ -> []
proofGoal : EditMode -> String -> Maybe (Term Metavariable)
proofGoal mode querys =
case mode of
proofGoal editMode querys =
case editMode of
Query -> run term 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 =
case (run program progs, proofGoal mode querys) of
tryProve editMode progs querys =
case (run program progs, proofGoal editMode querys) of
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
viewProofTree : EditMode -> String -> String -> String -> Html Msg
viewProofTree mode renderProgs progs querys = viewSection "Proof Tree" <|
viewProofTree : EditMode -> ResultMode -> String -> String -> String -> Html Msg
viewProofTree editMode resultMode renderProgs progs querys =
Html.div [ class "bergamot-proof-tree" ] <|
case tryProve mode progs querys of
Just tree ->
case tryProve editMode progs querys of
Just (MkProofTree tree) ->
case run program renderProgs of
Just renderProg ->
List.map latex
<| List.filterMap (renderTreeViaRules renderProg)
<| [ tree ]
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 -> []
view : Model -> Html Msg
view m = Html.div [ class "bergamot-root" ]
[ viewTabSelector m.tab [(Editor, "Rule Editor"), (MetaEditor, "Meta 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.renderProgram m.program m.query
, viewTab m.tab
(viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ])
(viewSection "Meta Rules" <| Html.textarea [ onInput SetRenderProgram ] [ Html.text m.renderProgram ])
(Html.Lazy.lazy2 viewRules m.renderProgram m.program)
[ viewSection "Input" <| Html.div []
[ viewEditModeSelector m.editMode [(Query, "Query"), (Syntax, "Language Term")]
, Html.input [ type_ "text", onInput SetQuery, value m.query ] []
]
, viewSection "Result" <| Html.div[]
[ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
, viewProofTree m.editMode m.resultMode m.renderProgram 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)
@ -151,6 +177,7 @@ update msg m =
SetQuery query -> ({ m | query = query }, Cmd.none)
SetTab tab -> ({ m | tab = tab }, Cmd.none)
SetEditMode mode -> ({ m | editMode = mode }, Cmd.none)
SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
subscriptions : Model -> Sub Msg
subscriptions _ = Sub.none