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

Add some styling (still very early stages)

This commit is contained in:
Danila Fedorin 2023-11-26 16:25:23 -08:00
parent 250dbb4ee8
commit 33c3f87564
2 changed files with 64 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
index.html
View File

@ -2,10 +2,45 @@
<html>
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title>Main</title>
<script type="module" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.esm.js"></script>
<script nomodule="" src="https://unpkg.com/@navsnpm/katex-expression/dist/katex-expression/katex-expression.js"></script>
<style>body { padding: 0; margin: 0; }</style>
<style>
textarea {
display: block;
width: 100%;
height: 10em;
resize: none;
}
input[type="text"] {
width: 100%;
}
.rule-list {
display: flex;
flex-direction: row;
flex-wrap: wrap;
justify-content: center;
}
.rule-list katex-expression {
margin-left: .5em;
margin-right: .5em;
flex-grow: 1;
flex-basis: 0;
}
.elm-root {
max-width: 800px;
margin: auto;
padding: 1em;
border: 1px solid #c3c3c3;
border-radius: 0.5em;
}
</style>
</head>
<body>

46
src/Main.elm
View File

@ -3,7 +3,7 @@ module Main exposing (main)
import Browser
import Html exposing (Html)
import Html.Events exposing (onInput)
import Html.Attributes exposing (type_)
import Html.Attributes exposing (type_, class)
import Bergamot.Syntax exposing (..)
import Bergamot.Search exposing (..)
import Bergamot.Rules exposing (..)
@ -26,28 +26,40 @@ type Msg
init : Flags -> (Model, Cmd Msg)
init () = ({ program = "", query = "" }, Cmd.none)
printRules : String -> Maybe String
printRules progs =
case run program progs of
Just prog -> Just (String.join "\n\\quad" (List.map ruleToLatex prog.rules))
Nothing -> Nothing
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
Html.div [] [ Html.h2 [] [ Html.text name ], content ]
proveQuery : String -> String -> Maybe ProofTree
proveQuery progs querys =
viewRule : Rule -> Html Msg
viewRule = latex << ruleToLatex
viewRules : String -> Html Msg
viewRules progs = viewSection "Rendered Rules" <|
Html.div [ class "rule-list" ] <|
case run program progs of
Just prog -> List.map viewRule prog.rules
Nothing -> []
tryProve : String -> String -> Maybe ProofTree
tryProve progs querys =
case (run program progs, run term querys) of
(Just prog, Just query) -> single prog (prove query |> Bergamot.Rules.andThen reifyProofTree)
_ -> Nothing
viewProofTree : String -> String -> Html Msg
viewProofTree progs querys = viewSection "Proof Tree" <|
Html.div [ class "proof-tree" ] <|
case tryProve progs querys of
Just tree -> [ latex (proofTreeToLatex tree) ]
Nothing -> []
view : Model -> Html Msg
view m = Html.div []
[ Html.textarea [ onInput SetProgram ] []
, Html.br [] []
, Html.input [ type_ "text", onInput SetQuery ] []
, latex (Maybe.withDefault "" (printRules m.program))
, latex (
proveQuery m.program m.query
|> Maybe.map proofTreeToLatex
|> Maybe.withDefault "")
view m = Html.div [ class "elm-root" ]
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery ] []
, viewRules m.program
, viewProofTree m.program m.query
]
update : Msg -> Model -> (Model, Cmd Msg)