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

Add flags for setting rules and query before starting

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-11-26 20:53:31 -08:00
parent f30752a2c6
commit 9d287a37d5
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
index.html
View File

@ -55,7 +55,8 @@ input[type="text"] {
<script src="index.js"></script>
<script>
var app = Elm.Main.init({
node: document.getElementById('elm')
node: document.getElementById('elm'),
flags: { rules: "TInt @ type(?Gamma, intlit(?n), tint) <-;\nTString @ type(?Gamma, strlit(?s), tstr) <-;\nTVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);\nTPlusI @ type(?Gamma, plus(?e_1, ?e_2), tint) <- type(?Gamma, ?e_1, tint), type(?Gamma, ?e_2, tint);\nTPlusS @ type(?Gamma, plus(?e_1, ?e_2), tstr) <- type(?Gamma, ?e_1, tstr), type(?Gamma, ?e_2, tstr);\nTPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <- type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);\nTFst @ type(?Gamma, fst(?e), ?tau_1) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTSnd @ type(?Gamma, snd(?e), ?tau_2) <- type(?Gamma, ?e, tpair(?tau_1, ?tau_2));\nTAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <- type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);\nTApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <- type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);\n\nGammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;\nGammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);", query: "type(empty, app(abs(x, tint, var(x)), intlit(1)), ?tau)" }
});
</script>
</body>

6
src/Main.elm
View File

@ -18,13 +18,13 @@ type alias Model =
{ program : String
, query : String
}
type alias Flags = ()
type alias Flags = { rules: String, query: String }
type Msg
= SetProgram String
| SetQuery String
init : Flags -> (Model, Cmd Msg)
init () = ({ program = "", query = "type(?e, tint)" }, Cmd.none)
init fs = ({ program = fs.rules, query = fs.query }, Cmd.none)
viewSection : String -> Html Msg -> Html Msg
viewSection name content =
@ -56,7 +56,7 @@ viewProofTree progs querys = viewSection "Proof Tree" <|
view : Model -> Html Msg
view m = Html.div [ class "elm-root" ]
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] []
[ viewSection "Rules" <| Html.textarea [ onInput SetProgram ] [ Html.text m.program ]
, viewSection "Query" <| Html.input [ type_ "text", onInput SetQuery, value m.query ] []
, viewRules m.program
, viewProofTree m.program m.query