From d1fb4bfdc1c94f553f00e0e041c719e9385542f2 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 7 Sep 2024 21:06:57 -0700
Subject: [PATCH] Update index.html to work with new setup

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 demorules.bergamot   | 28 ++++++++++++++++++++++++++++
 index.html           | 24 ++++++++++++++++++++----
 renderrules.bergamot | 12 ++++++++----
 3 files changed, 56 insertions(+), 8 deletions(-)
 create mode 100644 demorules.bergamot

diff --git a/demorules.bergamot b/demorules.bergamot
new file mode 100644
index 0000000..06aac80
--- /dev/null
+++ b/demorules.bergamot
@@ -0,0 +1,28 @@
+section "" {
+    TNumber @ type(?Gamma, lit(?n), number) <- num(?n);
+    TString @ type(?Gamma, lit(?s), string) <- str(?s);
+    TVar @ type(?Gamma, var(?x), ?tau) <- inenv(?x, ?tau, ?Gamma);
+    TPlusI @ type(?Gamma, plus(?e_1, ?e_2), number) <-
+        type(?Gamma, ?e_1, number), type(?Gamma, ?e_2, number);
+    TPlusS @ type(?Gamma, plus(?e_1, ?e_2), string) <-
+        type(?Gamma, ?e_1, string), type(?Gamma, ?e_2, string);
+}
+section "" {
+    TPair @ type(?Gamma, pair(?e_1, ?e_2), tpair(?tau_1, ?tau_2)) <-
+        type(?Gamma, ?e_1, ?tau_1), type(?Gamma, ?e_2, ?tau_2);
+    TFst @ type(?Gamma, fst(?e), ?tau_1) <-
+        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
+    TSnd @ type(?Gamma, snd(?e), ?tau_2) <-
+        type(?Gamma, ?e, tpair(?tau_1, ?tau_2));
+}
+section "" {
+    TAbs @ type(?Gamma, abs(?x, ?tau_1, ?e), tarr(?tau_1, ?tau_2)) <-
+        type(extend(?Gamma, ?x, ?tau_1), ?e, ?tau_2);
+    TApp @ type(?Gamma, app(?e_1, ?e_2), ?tau_2) <-
+        type(?Gamma, ?e_1, tarr(?tau_1, ?tau_2)), type(?Gamma, ?e_2, ?tau_1);
+}
+
+section "" {
+    GammaTake @ inenv(?x, ?tau_1, extend(?Gamma, ?x, ?tau_1)) <-;
+    GammaSkip @ inenv(?x, ?tau_1, extend(?Gamma, ?y, ?tau_2)) <- inenv(?x, ?tau_1, ?Gamma);
+}
diff --git a/index.html b/index.html
index b95e86c..00f58c1 100644
--- a/index.html
+++ b/index.html
@@ -54,10 +54,26 @@ input[type="text"] {
     <div id="elm"></div>
     <script src="index.js"></script>
     <script>
-        var app = Elm.Main.init({
-          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)" }
-        });
+        (async () => {
+            var rulesResponse = await fetch("./demorules.bergamot");
+            var rules = await rulesResponse.text();
+            var renderRulesResponse = await fetch("./renderrules.bergamot");
+            var renderRules = await renderRulesResponse.text();
+            console.log(rules);
+            var app = Elm.Main.init({
+                node: document.getElementById('elm'),
+                flags: {
+                    inputModes: {
+                        "Query": "query",
+                        "Language Term": "syntax",
+                        "My Mode": { "custom": "mymode" },
+                    },
+                    inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);",
+                    query: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)",
+                    renderRules: renderRules, rules: rules
+                }
+            });
+        })();
     </script>
 </body>
 </html>
diff --git a/renderrules.bergamot b/renderrules.bergamot
index b13c72b..e86019b 100644
--- a/renderrules.bergamot
+++ b/renderrules.bergamot
@@ -28,10 +28,10 @@ IntercalateConsNil @ intercalate(?sep, cons(?x, nil), cons(?x, nil)) <-;
 NonEmpty @ nonempty(cons(?x, ?xs)) <-;
 
 LatexInt @ latex(?i, ?l) <- int(?i), tostring(?i, ?l);
+LatexFloat @ latex(?f, ?l) <- float(?f), tostring(?f, ?l);
 LatexStr @ latex(?s, ?l) <- str(?s), escapestring(?s, ?l_1), latexifystring(?s, ?l_2), join(["\\texttt{\"", ?l_2, "\"}"], ?l);
 LatexMeta @ latex(metavariable(?l), ?l) <-;
-LatexIntLit @ latex(intlit(?i), ?l) <- latex(?i, ?l);
-LatexStrLit @ latex(strlit(?s), ?l) <- latex(?s, ?l);
+LatexLit @ latex(lit(?i), ?l) <- latex(?i, ?l);
 LatexVar @ latex(var(?s), ?l) <- latex(?s, ?l);
 LatexPlus @ latex(plus(?e_1, ?e_2), ?l) <-
     latex(?e_1, ?l_1), latex(?e_2, ?l_2),
@@ -62,7 +62,11 @@ LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t)
 LatexTypeBin @ latex(type(?e, ?t), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), join([?l_e, " : ", ?l_t], ?l);
 LatexTypeTer @ latex(type(?G, ?e, ?t), ?l) <- latex(?G, ?l_G), latex(?e, ?l_e), latex(?t, ?l_t), join([?l_G, " \\vdash ", ?l_e, " : ", ?l_t], ?l);
 
-LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\mathbb{Z}"], ?l);
-LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\mathbb{S}"], ?l);
+LatexConverts @ latex(converts(?f, ?t), ?l) <- latex(?f, ?l_f), latex(?t, ?l_t), join([?l_f, " \\preceq ", ?l_t], ?l);
+
+LatexIsInt @ latex(int(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Int}"], ?l);
+LatexIsFloat @ latex(float(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Float}"], ?l);
+LatexIsNum @ latex(num(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Num}"], ?l);
+LatexIsStr @ latex(str(?e), ?l) <- latex(?e, ?l_e), join([?l_e, " \\in \\texttt{Str}"], ?l);
 LatexSym @ latex(?s, ?l) <- sym(?s), tostring(?s, ?l_1), join(["\\text{", ?l_1,"}"], ?l);
 LatexCall @ latex(?c, ?l) <- call(?c, ?n, ?ts), nonempty(?ts), latexlist(?ts, ?lts_1), intercalate(", ", ?lts_1, ?lts_2), join(?lts_2, ?lts_3), join(["\\text{", ?n, "}", "(", ?lts_3, ")"], ?l);