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"] {