From 9d287a37d5d893c87d0772a3b21b814cdfca43cf Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 26 Nov 2023 20:53:31 -0800
Subject: [PATCH] Add flags for setting rules and query before starting

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 index.html   | 3 ++-
 src/Main.elm | 6 +++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/index.html b/index.html
index 2bd73a9..b95e86c 100644
--- a/index.html
+++ b/index.html
@@ -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>
diff --git a/src/Main.elm b/src/Main.elm
index 7d4e446..8df1b8d 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -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