Use stable version of NixOS for nixpkgs

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
Update flake.lock
2025-12-26 22:30:08 +00:00 · 2025-12-26 21:25:04 +00:00 · 2024-11-03 17:13:14 -08:00 · 2024-11-03 17:13:05 -08:00 · 2024-09-15 16:33:07 -07:00 · 2024-09-15 10:21:38 -07:00
14 changed files with 1049 additions and 121 deletions
--- a/demorules.bergamot
+++ 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);
+}
--- a/elm.nix
+++ b/elm.nix
@@ -29,7 +29,7 @@ let
        mkdir -p $out/share/doc
        ${lib.concatStrings (map (module: ''
          echo "compiling ${elmfile module}"
-          elm make ${elmfile module} --output $out/${module}.${extension} --docs $out/share/doc/${module}.json
+          elm make ${elmfile module} --output $out/${module}.${extension} --docs $out/share/doc/${module}.json --optimize
          ${lib.optionalString outputJavaScript ''
            echo "minifying ${elmfile module}"
            uglifyjs $out/${module}.${extension} --compress 'pure_funcs="F2,F3,F4,F5,F6,F7,F8,F9,A2,A3,A4,A5,A6,A7,A8,A9",pure_getters,keep_fargs=false,unsafe_comps,unsafe' \
@@ -42,7 +42,7 @@ in mkDerivation {
  name = "bergamot-elm";
  srcs = ./elm-dependencies.nix;
  src = ./.;
-  targets = ["Main"];
+  targets = ["Main" "Bergamot.ObjectLanguage"];
  srcdir = "./src";
  outputJavaScript = true;
 }
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
        "systems": "systems"
      },
      "locked": {
-        "lastModified": 1694529238,
-        "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
        "owner": "numtide",
        "repo": "flake-utils",
-        "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
        "type": "github"
      },
      "original": {
@@ -20,16 +20,16 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1701068326,
-        "narHash": "sha256-vmMceA+q6hG1yrjb+MP8T0YFDQIrW3bl45e7z24IEts=",
+        "lastModified": 1766736597,
+        "narHash": "sha256-BASnpCLodmgiVn0M1MU2Pqyoz0aHwar/0qLkp7CjvSQ=",
        "owner": "nixos",
        "repo": "nixpkgs",
-        "rev": "8cfef6986adfb599ba379ae53c9f5631ecd2fd9c",
+        "rev": "f560ccec6b1116b22e6ed15f4c510997d99d5852",
        "type": "github"
      },
      "original": {
        "owner": "nixos",
-        "ref": "nixos-unstable",
+        "ref": "nixos-25.11",
        "repo": "nixpkgs",
        "type": "github"
      }
--- a/flake.nix
+++ b/flake.nix
@@ -1,6 +1,6 @@
 {
  inputs = {
-    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-25.11";
    flake-utils.url = "github:numtide/flake-utils";
  };
  outputs = { self, nixpkgs, flake-utils }:
--- a/index.html
+++ b/index.html
@@ -53,11 +53,42 @@ input[type="text"] {
 <body>
    <div id="elm"></div>
    <script src="index.js"></script>
+    <script src="language.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)" }
-        });
+        const objectLang = Elm.Bergamot.ObjectLanguage.init({});
+
+        (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: {
+                        "Language Term": { "custom": "langterm" },
+                        "Query": "query",
+                    },
+                    inputRules: "PromptConverter @ prompt(type(empty, ?term, ?t)) <- input(?term);",
+                    input: "type(empty, app(abs(x, number, var(x)), lit(1)), ?tau)",
+                    renderRules: renderRules, rules: rules
+                }
+            });
+
+            objectLang.ports.parsedString.subscribe(({ string, term }) => {
+                if (term !== null) {
+                    const query = `type(empty, ${term}, ?tau)`;
+                    app.ports.receiveConverted.send({ input: string, result: { query } });
+                } else {
+                    app.ports.receiveConverted.send({ input: string, result: { error: "Unable to parse object language term" } });
+                }
+            });
+
+            app.ports.convertInput.subscribe(({ mode, input }) => {
+                objectLang.ports.parseString.send(input);
+            });
+        })();
    </script>
 </body>
 </html>
--- a/renderrules.bergamot
+++ b/renderrules.bergamot
@@ -0,0 +1,72 @@
+PrecApp @ prec(app(?l, ?r), 100, left) <-;
+PrecPlus @ prec(plus(?l, ?r), 80, either) <-;
+PrecAbs @ prec(abs(?x, ?t, ?e), 0, right) <-;
+PrecArr @ prec(tarr(?l, ?r), 0, right) <-;
+
+SelectHead @ select(cons([?t, ?v], ?rest), ?default, ?v) <- ?t;
+SelectTail @ select(cons([?t, ?v], ?rest), ?default, ?found) <- not(?t), select(?rest, ?default, ?found);
+SelectEmpty @ select(nil, ?default, ?default) <-;
+
+ParenthAssocLeft @ parenthassoc(?a_i, left, right) <-;
+ParenthAssocRight @ parenthassoc(?a_i, right, left) <-;
+ParenthAssocNone @ parenthassoc(?a_i, none, ?pos) <-;
+ParenthAssocNeq @ parenthassoc(?a_i, ?a_o, ?pos) <- not(symeq(?a_i, ?a_o));
+
+Parenth @ parenth(?inner, ?outer, ?pos, ?strin, ?strout) <-
+    prec(?inner, ?p_i, ?a_i), prec(?outer, ?p_o, ?a_o),
+    join(["(", ?strin, ")"], ?strinparen),
+    select([ [less(?p_i, ?p_o), strinparen], [less(?p_o, ?p_i), ?strin], [ parenthassoc(?a_i, ?a_o, ?pos), ?strinparen ] ], ?strin, ?strout);
+ParenthFallback @ parenth(?inner, ?outer, ?pos, ?strin, ?strin) <-;
+
+LatexListNil @ latexlist(nil, nil) <-;
+LatexListCons @ latexlist(cons(?x, ?xs), cons(?l_x, ?l_s)) <- latex(?x, ?l_x), latexlist(?xs, ?l_s);
+
+IntercalateNil @ intercalate(?sep, nil, nil) <-;
+IntercalateConsCons @ intercalate(?sep, cons(?x_1, cons(?x_2, ?xs)), cons(?x_1, cons(?sep, ?ys))) <- intercalate(?sep, cons(?x_2, ?xs), ?ys);
+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) <-;
+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),
+    parenth(?e_1, plus(?e_1, ?e_2), left, ?l_1, ?lp_1),
+    parenth(?e_2, plus(?e_1, ?e_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " + ", ?lp_2], ?l);
+LatexPair @ latex(pair(?e_1, ?e_2), ?l) <- latex(?e_1, ?l_1), latex(?e_2, ?l_2), join(["(", ?l_1, ",  ", ?l_2, ")"], ?l);
+LatexAbs @ latex(abs(?x, ?t, ?e), ?l) <- latex(?e, ?l_e), latex(?t, ?l_t), latex(?x, ?l_x), join(["\\lambda ", ?l_x, " : ", ?l_t, " . ", ?l_e], ?l);
+LatexApp @ latex(app(?e_1, ?e_2), ?l) <-
+    latex(?e_1, ?l_1), latex(?e_2, ?l_2),
+    parenth(?e_1, app(?e_1, ?e_2), left, ?l_1, ?lp_1),
+    parenth(?e_2, app(?e_1, ?e_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " \\enspace ", ?lp_2], ?l);
+
+LatexTInt @ latex(tint, "\\text{tint}") <-;
+LatexTStr @ latex(tstr, "\\text{tstr}") <-;
+LatexTArr @ latex(tarr(?t_1, ?t_2), ?l) <-
+    latex(?t_1, ?l_1), latex(?t_2, ?l_2),
+    parenth(?t_1, tarr(?t_1, ?t_2), left, ?l_1, ?lp_1),
+    parenth(?t_2, tarr(?t_1, ?t_2), right, ?l_2, ?lp_2),
+    join([?lp_1, " \\to ", ?lp_2], ?l);
+LatexTPair @ latex(tpair(?t_1, ?t_2), ?l) <- latex(?t_1, ?l_1), latex(?t_2, ?l_2), join(["(", ?l_1, ", ", ?l_2, ")"], ?l);
+
+LatexTypeEmpty @ latex(empty, "\\varnothing") <-;
+LatexTypeExtend @ latex(extend(?a, ?b, ?c), ?l) <- latex(?a, ?l_a), latex(?b, ?l_b), latex(?c, ?l_c), join([?l_a, " , ", ?l_b, " : ", ?l_c], ?l);
+LatexTypeInenv @ latex(inenv(?x, ?t, ?G), ?l) <-latex(?x, ?l_x), latex(?t, ?l_t), latex(?G, ?l_G), join([?l_x, " : ", ?l_t, " \\in ", ?l_G], ?l);
+
+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);
+
+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);
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@@ -1,30 +1,66 @@
 module Bergamot.Latex exposing (..)

-import Bergamot.Syntax exposing (..)
-import Bergamot.Rules exposing (..)
+import Bergamot.Syntax as Syntax exposing (..)
+import Bergamot.Rules as Rules exposing (..)
+import Bergamot.Utils exposing (..)

-termToLatex : (a -> String) -> Term a -> String
-termToLatex f t =
-    case t of
-        Call "intlit" [t1]   -> termToLatex f t1
-        Call "strlit" [t1]   -> termToLatex f t1
-        Call "var" [t1]   -> termToLatex f t1
-        Call "plus" [t1, t2] -> termToLatex f t1 ++ " + " ++ termToLatex f t2
-        Call "pair" [t1, t2] -> "(" ++ termToLatex f t1 ++ ", " ++ termToLatex f t2 ++ ")"
-        Call "abs" [t1, t2, t3] -> "\\lambda " ++ termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ ".\\ " ++ termToLatex f t3
-        Call "app" [t1, t2] -> termToLatex f t1 ++ "\\ " ++ termToLatex f t2
-        Call "type" [t1, t2] -> termToLatex f t1 ++ " : " ++ termToLatex f t2
-        Call "type" [t1, t2, t3] -> termToLatex f t1 ++ "\\vdash " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
-        Call "tpair" [t1, t2] -> termToLatex f t1 ++ "\\times" ++ termToLatex f t2
-        Call "tarr" [t1, t2] -> termToLatex f t1 ++ "\\to" ++ termToLatex f t2
-        Call "extend" [t1, t2, t3] -> termToLatex f t1 ++ ",\\ " ++ termToLatex f t2 ++ " : " ++ termToLatex f t3
-        Call "inenv" [t1, t2, t3] -> termToLatex f t1 ++ " : " ++ termToLatex f t2 ++ " \\in " ++ termToLatex f t3 
-        Call "empty" [] -> "\\varnothing"
-        Call s [] -> "\\text{" ++ s ++ "}"
-        Call s ts -> "\\text{" ++ s ++ "}(" ++ String.join "," (List.map (termToLatex f) ts) ++ ")"
-        Var x -> f x
-        IntLit i -> String.fromInt i
-        StringLit s -> "\"" ++ s ++ "\""
+import Debug
+
+type Void = Void Void
+
+absurd : Void -> a
+absurd (Void v) = absurd v
+
+renderTermViaRules : RuleEnv -> Term Void -> Maybe String
+renderTermViaRules env t =
+    Call "latex" [Syntax.map absurd t, Var (MkMetavariable "s")]
+    |> prove
+    |> Rules.andThen reifyProofTree
+    |> single env
+    |> Maybe.andThen (\(MkProofTree node) ->
+        case node.conclusion of
+            Call "latex" [_, StringLit s] -> Just s
+            _ -> Nothing)
+
+buildInferenceRuleFrac : List String -> String -> String -> String
+buildInferenceRuleFrac prems conc name = String.concat
+    [ "\\cfrac{"
+    ,   String.join "\\quad " prems
+    , "}{"
+    ,   conc
+    , "}\\ \\texttt{"
+    ,   name
+    , "}"
+    ]
+
+renderRuleViaRules : RuleEnv -> Rule -> Maybe String
+renderRuleViaRules env r =
+    let
+        quotedPrems = List.map quoteMetavariables r.premises
+        quotedConc = quoteMetavariables r.conclusion
+    in
+        renderTermViaRules env quotedConc
+        |> Maybe.andThen (\conc ->
+            sequenceMaybes (List.map (renderTermViaRules env) quotedPrems)
+            |> Maybe.map (\prems -> buildInferenceRuleFrac prems conc r.name))
+
+renderTreeViaRules : RuleEnv -> ProofTree -> Maybe String
+renderTreeViaRules env (MkProofTree node) =
+    renderTermViaRules env (quoteVariables node.conclusion)
+    |> Maybe.andThen (\conc ->
+        sequenceMaybes (List.map (renderTreeViaRules env) node.premises)
+        |> Maybe.map (\prems -> buildInferenceRuleFrac prems conc node.name))
+
+quote : String -> (a -> String) -> Term a -> Term Void
+quote s f =
+    let helper a = Call s [StringLit <| f a]
+    in Syntax.andThen helper
+
+quoteMetavariables : Term Metavariable -> Term Void
+quoteMetavariables = quote "metavariable" metavariableToLatex
+
+quoteVariables : Term UnificationVar -> Term Void
+quoteVariables = quote "variable" (\(MkUnificationVar v) -> v)

 metavariableToLatex : Metavariable -> String
 metavariableToLatex (MkMetavariable s) =
@@ -32,13 +68,5 @@ metavariableToLatex (MkMetavariable s) =
        noQuestion = String.dropLeft 1 s
    in
        if String.startsWith "tau" noQuestion then "\\" ++ noQuestion else
-        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else noQuestion
-
-ruleToLatex : Rule -> String
-ruleToLatex r = "\\cfrac{" ++ String.join "\\quad " (List.map (termToLatex metavariableToLatex) r.premises) ++ "}{" ++ termToLatex metavariableToLatex r.conclusion ++ "}\\ \\texttt{" ++ r.name ++ "}"
-
-unificationVarToLatex : UnificationVar -> String
-unificationVarToLatex (MkUnificationVar s) = s
-
-proofTreeToLatex : ProofTree -> String
-proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
+        if String.startsWith "Gamma" noQuestion then "\\" ++ noQuestion else
+        if String.startsWith "rho" noQuestion then "\\" ++ noQuestion else noQuestion
--- a/src/Bergamot/ObjectLanguage.elm
+++ b/src/Bergamot/ObjectLanguage.elm
@@ -0,0 +1,192 @@
+port module Bergamot.ObjectLanguage exposing (..)
+
+import Bergamot.Syntax as Syntax exposing (toString)
+import Bergamot.Parser exposing (strLit)
+
+import Platform exposing (worker)
+import Parser exposing (Parser, Trailing(..), (|.), (|=), run)
+import Set
+
+type Type
+    = TInt
+    | TStr
+    | TPair Type Type
+    | TArr Type Type
+
+type Expr
+    = IntLit Int
+    | FloatLit Float
+    | StrLit String
+    | Plus Expr Expr
+    | Pair Expr Expr
+    | Fst Expr
+    | Snd Expr
+    | Abs String Type Expr
+    | App Expr Expr
+    | Ref String
+
+parenthed : Parser a -> Parser a
+parenthed val = Parser.succeed (\x -> x)
+    |. Parser.symbol "("
+    |. Parser.spaces
+    |= val
+    |. Parser.spaces
+    |. Parser.symbol ")"
+
+pair : Parser a -> Parser (a, a)
+pair elem = parenthed <|
+    Parser.succeed Tuple.pair
+    |= elem
+    |. Parser.spaces
+    |. Parser.symbol ","
+    |. Parser.spaces
+    |= elem
+
+type_ : Parser Type
+type_ = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable <| Parser.succeed TArr
+        |= typeBasic
+        |. Parser.spaces
+        |. Parser.symbol "->"
+        |. Parser.spaces
+        |= type_
+    , typeBasic
+    ]
+
+typeBasic : Parser Type
+typeBasic = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.succeed TInt |. Parser.keyword "number"
+    , Parser.succeed TStr |. Parser.keyword "string"
+    , Parser.backtrackable <| Parser.map (\(a, b) -> TPair a b) <| pair type_
+    , parenthed type_
+    ]
+
+variable : Parser String
+variable = Parser.variable
+    { start = Char.isAlphaNum
+    , inner = Char.isAlphaNum
+    , reserved = Set.fromList ["fst", "snd", "let", "in"]
+    }
+
+expr : Parser Expr
+expr = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable <| Parser.succeed Plus
+        |= exprBasic
+        |. Parser.spaces
+        |. Parser.symbol "+"
+        |. Parser.spaces
+        |= expr
+    , exprApps
+    ]
+
+topLevelExpr : Parser Expr
+topLevelExpr = expr |. Parser.end
+
+exprApps : Parser Expr
+exprApps =
+    let
+        handle l =
+            case l of
+                [] -> Parser.problem "no applications found"
+                x :: xs -> Parser.succeed <| List.foldl (\a b -> App b a) x xs
+    in
+        Parser.sequence
+            { start = ""
+            , separator = " "
+            , end = ""
+            , spaces = Parser.succeed ()
+            , item = exprBasic
+            , trailing = Optional
+            }
+        |> Parser.andThen handle
+
+exprBasic : Parser Expr
+exprBasic = Parser.lazy <| \() -> Parser.oneOf
+    [ Parser.backtrackable <|
+      Parser.number
+        { int = Just IntLit
+        , hex = Nothing
+        , octal = Nothing
+        , binary = Nothing
+        , float = Just FloatLit
+        }
+    , Parser.backtrackable (Parser.succeed StrLit |= strLit)
+    , Parser.backtrackable <| Parser.map (\(a, b) -> Pair a b) <| pair expr
+    , Parser.succeed Fst
+        |. Parser.keyword "fst"
+        |. Parser.spaces
+        |= parenthed expr
+    , Parser.succeed Snd
+        |. Parser.keyword "snd"
+        |. Parser.spaces
+        |= parenthed expr
+    , Parser.succeed Abs
+        |. Parser.symbol "\\"
+        |. Parser.spaces
+        |= variable
+        |. Parser.spaces
+        |. Parser.symbol ":"
+        |. Parser.spaces
+        |= type_
+        |. Parser.spaces
+        |. Parser.symbol "."
+        |. Parser.spaces
+        |= expr
+    , Parser.succeed Ref |= variable
+    , parenthed expr
+    ]
+
+typeToTerm : Type -> Syntax.Term ()
+typeToTerm t =
+    case t of
+        TInt -> Syntax.Call "number" []
+        TStr -> Syntax.Call "string" []
+        TPair t1 t2 -> Syntax.Call "tpair" [ typeToTerm t1, typeToTerm t2 ]
+        TArr t1 t2 -> Syntax.Call "tarr" [ typeToTerm t1, typeToTerm t2 ]
+
+exprToTerm : Expr -> Syntax.Term ()
+exprToTerm e =
+    case e of
+        IntLit i -> Syntax.Call "lit" [Syntax.IntLit i]
+        FloatLit f -> Syntax.Call "lit" [Syntax.FloatLit f]
+        StrLit s -> Syntax.Call "lit" [Syntax.StringLit s]
+        Plus e1 e2 -> Syntax.Call "plus" [exprToTerm e1, exprToTerm e2]
+        Pair e1 e2 -> Syntax.Call "pair" [exprToTerm e1, exprToTerm e2]
+        Fst ep -> Syntax.Call "fst" [exprToTerm ep]
+        Snd ep -> Syntax.Call "snd" [exprToTerm ep]
+        Abs s t ep -> Syntax.Call "abs" [Syntax.Call s [], typeToTerm t, exprToTerm ep]
+        App e1 e2 -> Syntax.Call "app" [exprToTerm e1, exprToTerm e2]
+        Ref x -> Syntax.Call "var" [Syntax.Call x []]
+
+-- Receives requests from JS code to apply the parser
+port parseString : (String -> msg) -> Sub msg
+
+-- Used to send the result of parsing back to JS
+port parsedString : { string : String, term : Maybe String } -> Cmd msg
+
+type Msg = ParseString String
+type alias Model = ()
+type alias Flags = ()
+
+init : Flags -> (Model, Cmd Msg)
+init _ = ((), Cmd.none)
+
+update : Msg -> Model -> (Model, Cmd Msg)
+update (ParseString s) _ =
+    case run topLevelExpr s of
+        Ok e ->
+            ( ()
+            , parsedString
+                { string = s
+                , term =
+                    exprToTerm e
+                    |> toString (\_ -> "")
+                    |> Just
+                }
+            )
+        Err _ -> ((), parsedString { string = s, term = Nothing })
+
+subscriptions : Model -> Sub Msg
+subscriptions _ = parseString ParseString
+
+main = worker { init = init, update = update, subscriptions = subscriptions }
--- a/src/Bergamot/Parser.elm
+++ b/src/Bergamot/Parser.elm
@@ -1,19 +1,41 @@
 module Bergamot.Parser exposing (..)

 import Bergamot.Syntax exposing (Term(..), Metavariable(..))
-import Bergamot.Rules exposing (Rule, RuleEnv)
+import Bergamot.Rules exposing (Rule, Section, RuleEnv)
+import Bergamot.Utils exposing (decodeStr)

 import Parser exposing (Parser, Trailing(..), (|.), (|=))
-import Set
+import Set exposing (Set)
+
+reserved : Set String
+reserved = Set.fromList ["hidden", "section"]
+
+strLit : Parser String
+strLit =
+    let
+        char = Parser.map decodeStr <| Parser.getChompedString <|
+            Parser.oneOf
+                [ Parser.backtrackable <|
+                    Parser.chompIf (\c -> c == '\\')
+                    |. Parser.chompIf (\c -> True)
+                , Parser.backtrackable <| Parser.chompIf (\c -> c /= '"')
+                ]
+    in
+        Parser.map (String.join "") <| Parser.sequence
+            { start = "\""
+            , separator = ""
+            , end = "\""
+            , spaces = Parser.succeed ()
+            , item = char
+            , trailing = Optional
+            }

-intLit : Parser Int
-intLit = Parser.int

 name : Parser String
 name = Parser.variable
-    { start = \c -> Char.isAlphaNum c || c == '_'
+    { start = \c -> Char.isAlpha c || c == '_'
    , inner = \c -> Char.isAlphaNum c || c == '_'
-    , reserved = Set.empty
+    , reserved = reserved
    }

 variable : Parser Metavariable
@@ -22,7 +44,7 @@ variable =
    |= Parser.variable
        { start = \c -> c == '?'
        , inner = \c -> Char.isAlphaNum c || c == '_'
-        , reserved = Set.empty
+        , reserved = reserved
        }

 term : Parser (Term Metavariable)
@@ -38,14 +60,34 @@ term = Parser.lazy (\() -> Parser.oneOf
            , item = term
            , trailing = Forbidden
            }
+    , Parser.backtrackable
+        <| Parser.map (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []))
+        <| Parser.sequence
+            { start = "["
+            , separator = ","
+            , end = "]"
+            , spaces = Parser.spaces
+            , item = term
+            , trailing = Forbidden
+            }
    , Parser.backtrackable <|
      Parser.succeed (\n -> Call n [])
        |= name
    , Parser.backtrackable <|
      Parser.succeed Var |= variable
-    , Parser.succeed IntLit |= intLit
+    , Parser.number
+        { int = Just IntLit
+        , hex = Nothing
+        , octal = Nothing
+        , binary = Nothing
+        , float = Just FloatLit
+        }
+    , Parser.succeed StringLit |= strLit
    ])

+topLevelTerm : Parser (Term Metavariable)
+topLevelTerm = term |. Parser.end
+
 rule : Parser Rule
 rule =
    let
@@ -64,16 +106,54 @@ rule =
            , item = term
            , trailing = Forbidden
            }
+        |. Parser.spaces |. Parser.symbol ";" |. Parser.spaces
+
+rules : Parser (List Rule)
+rules = Parser.sequence
+    { start = ""
+    , separator = ""
+    , end = ""
+    , spaces = Parser.spaces
+    , item = rule
+    , trailing = Optional
+    }
+
+sectionExp : Parser Section
+sectionExp =
+    Parser.succeed (\h n rs -> { hidden = h, name = n, rules = rs })
+    |= Parser.oneOf
+        [ Parser.succeed True
+          |. Parser.symbol "hidden"
+          |. Parser.spaces
+        , Parser.succeed False
+        ]
+    |. Parser.symbol "section" |. Parser.spaces
+    |= strLit |. Parser.spaces
+    |. Parser.symbol "{" |. Parser.spaces
+    |= rules
+    |. Parser.symbol "}" |. Parser.spaces
+
+sectionImp : Parser Section
+sectionImp =
+    (\rs ->
+        Parser.oneOf
+            [ rule |> Parser.map (\r -> Parser.Loop <| r :: rs)
+            , case rs of
+                [] -> Parser.problem "empty implicit sections not allowed."
+                _ -> Parser.succeed (Parser.Done <| List.reverse rs)
+            ])
+    |> Parser.loop []
+    |> Parser.map (\rs -> { hidden = False, name = "", rules = rs })

 program : Parser RuleEnv
 program =
-    Parser.succeed (\rs -> { rules = rs })
+    Parser.succeed (\ss -> { sections = ss })
    |= Parser.sequence
        { start = ""
-        , separator = ";"
+        , separator = ""
        , end = ""
        , spaces = Parser.spaces
-        , item = rule
+        , item = Parser.oneOf [sectionExp, sectionImp]
        , trailing = Mandatory
        }
    |. Parser.end
--- a/src/Bergamot/Rules.elm
+++ b/src/Bergamot/Rules.elm
@@ -1,7 +1,8 @@
 module Bergamot.Rules exposing (..)

-import Bergamot.Syntax exposing (Term, Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
+import Bergamot.Syntax exposing (Term(..), Metavariable, UnificationVar, unify, emptyUnificationState, instantiate, instantiateList, emptyInstantiationState, resetVars, InstantiationState, UnificationState, reify)
 import Bergamot.Search as Search exposing (Search)
+import Bergamot.Utils exposing (encodeStr, encodeLatex)

 import Debug

@@ -11,6 +12,12 @@ type alias Rule =
    , premises : List (Term Metavariable)
    }

+type alias Section =
+    { name : String
+    , rules : List Rule
+    , hidden: Bool
+    }
+
 type ProofTree = MkProofTree
    { name : String
    , conclusion : Term UnificationVar
@@ -18,7 +25,7 @@ type ProofTree = MkProofTree
    }

 type alias RuleEnv =
-    { rules : List Rule
+    { sections : List Section
    }

 type alias ProveState =
@@ -32,7 +39,7 @@ type alias Prover a = RuleEnv -> ProveState -> Search (a, ProveState)
 andThen : (a -> Prover b) -> Prover a -> Prover b
 andThen f p env ps =
    p env ps
-    |> Search.andThen (\(a, psp) -> if psp.gas > 0 then (f a) env psp else Search.fail)
+    |> Search.andThen (\(a, psp) -> (f a) env psp)

 join : Prover (Prover a) -> Prover a
 join p = andThen (\x -> x) p
@@ -61,6 +68,9 @@ interleave p1 p2 env ps =
 pure : a -> Prover a
 pure a env ps = Search.pure (a, ps)

+lazy : (() -> Prover a) -> Prover a
+lazy f env ps = Search.lazy ((\p -> p env ps) << f)
+
 fail : Prover a
 fail env ps = Search.fail

@@ -70,11 +80,21 @@ yield p env ps = Search.yield (p env ps)
 getEnv : Prover RuleEnv
 getEnv env ps = Search.pure (env, ps)

+getRules : Prover (List Rule)
+getRules env ps = Search.pure (List.concatMap (.rules) env.sections, ps)
+
 getUnificationState : Prover UnificationState
 getUnificationState env ps = Search.pure (ps.unificationState, ps)

-burn : Prover ()
-burn env ps = Search.pure ((), { ps | gas = ps.gas - 1})
+burn : Prover a -> Prover a
+burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
+
+try : Prover a -> Prover (Maybe a)
+try p env ps =
+    p env { ps | gas = 30 }
+    |> Search.one
+    |> Maybe.map (Tuple.first << Tuple.first)
+    |> (\mx -> Search.pure (mx, ps))

 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
@@ -104,29 +124,109 @@ reifyProofTree (MkProofTree node) =
 rule : Term UnificationVar -> Rule -> Prover ProofTree
 rule t r =
        withVars (pure Tuple.pair
-            |> apply (liftInstantiation instantiate r.conclusion)
+            |> apply (liftInstantiation instantiate r.conclusion
+                |> andThen (\conc -> liftUnification unify t conc))
            |> apply (liftInstantiation instantiateList r.premises))
        |> andThen (\(conc, prems) ->
-            pure (\tp trees -> MkProofTree { name = r.name, conclusion = tp, premises = trees })
-            |> apply (liftUnification unify t conc)
-            |> apply (provePremises prems))
+            provePremises prems)
+            |> map (\trees -> MkProofTree { name = r.name, conclusion = t, premises = trees })
+
+collectStrings : Term UnificationVar -> Prover (List String)
+collectStrings t =
+    case t of
+        Call "cons" [StringLit s, rest] -> map (\ss -> s :: ss) <| collectStrings rest
+        Call "nil" [] -> pure []
+        _ -> fail
+
+builtinRules : Term UnificationVar -> Prover ProofTree
+builtinRules t =
+    let
+        suggest r v output =
+            liftUnification unify (Var output) v
+            |> map (\_ -> MkProofTree { name = r, conclusion = t, premises = [] })
+    in
+        case t of
+            Call "concat" [StringLit s1, StringLit s2, Var output] ->
+                liftUnification unify (Var output) (StringLit (s1 ++ s2))
+                |> map (\_ -> MkProofTree { name = "BuiltinConcat", conclusion = t, premises = []})
+            Call "join" [tp, Var output] ->
+                collectStrings tp
+                |> andThen (\ss -> liftUnification unify (Var output) (StringLit (String.concat ss)))
+                |> map (\_ -> MkProofTree { name = "BuiltinJoin", conclusion = t, premises = []})
+            Call "int" [IntLit i] ->
+                MkProofTree { name = "BuiltinInt", conclusion = t, premises = [] }
+                |> pure
+            Call "int" [Var output] ->
+                let rec i = interleave (suggest "BuiltinInt" (IntLit i) output) (lazy <| \_ -> rec (i+1))
+                in rec 0
+            Call "add" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinAdd" (IntLit (i1 + i2)) output
+            Call "subtract" [IntLit i1, IntLit i2, Var output] ->
+                suggest "BuiltinSubtract" (IntLit (i1 - i2)) output
+            Call "float" [FloatLit f] ->
+                MkProofTree { name = "BuiltinFloat", conclusion = t, premises = [] }
+                |> pure
+            Call "float" [Var output] ->
+                let rec f = interleave (suggest "BuiltinFloat" (FloatLit f) output) (lazy <| \_ -> rec (f+1))
+                in rec 0
+            Call "num" [tp] ->
+                interleave (builtinRules (Call "int" [tp])) (builtinRules (Call "float" [tp]))
+                |> map (\prem -> MkProofTree { name = "BuiltinNum", conclusion = t, premises = [prem] })
+            Call "str" [StringLit s] ->
+                MkProofTree { name = "BuiltinStr", conclusion = t, premises = [] }
+                |> pure
+            Call "str" [Var output] ->
+                List.foldr (\s -> interleave (suggest "BuiltinStr" (StringLit s) output)) fail
+                <| String.split "" "abcdefghijklmnopqrstuvwxyz"
+            Call "sym" [Call s []] ->
+                MkProofTree { name = "BuiltinSym", conclusion = t, premises = [] }
+                |> pure
+            Call "call" [Call s ts, Var name, Var args] ->
+                pure (\_ _ -> MkProofTree { name = "BuiltinCall", conclusion = t, premises = [] })
+                |> apply (liftUnification unify (Var name) (StringLit <| encodeStr s))
+                |> apply (liftUnification unify (Var args) (List.foldr (\x xs -> Call "cons" [x, xs]) (Call "nil" []) ts))
+            Call "tostring" [tp, Var output] ->
+                let
+                    suggestStr s = suggest "BuiltinToString" (StringLit s) output
+                in
+                    case tp of
+                        IntLit i -> suggestStr (String.fromInt i)
+                        FloatLit f -> suggestStr (String.fromFloat f)
+                        Call s [] -> suggestStr (encodeStr s)
+                        _ -> fail
+            Call "escapestring" [StringLit s, Var output] ->
+                liftUnification unify (Var output) (StringLit (encodeStr s))
+                |> map (\_ -> MkProofTree { name = "BuiltinEscapeString", conclusion = t, premises = []})
+            Call "latexifystring" [StringLit s, Var output] ->
+                liftUnification unify (Var output) (StringLit (encodeLatex s))
+                |> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
+            Call "not" [tp] ->
+                try (proveTerm tp)
+                |> andThen (\mp ->
+                    case mp of
+                        Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
+                        Just _ -> fail)
+            _ -> fail

 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)
 provePremises = mapM proveTerm

 proveTerm : Term UnificationVar -> Prover ProofTree
 proveTerm t =
-    burn
-    |> andThen (\() -> getEnv)
-    |> andThen (\env -> List.foldl (\r -> interleave (yield (rule t r))) fail env.rules)
+    getUnificationState
+    |> map (\us -> reify t us)
+    |> andThen (\tp ->
+        burn (
+            getRules
+            |> andThen (List.foldr (\r -> interleave ((rule tp r))) (builtinRules tp))))

 prove : Term Metavariable -> Prover ProofTree
 prove mt =
-    liftInstantiation instantiate mt
+    withVars (liftInstantiation instantiate mt)
    |> andThen proveTerm

 single : RuleEnv -> Prover a -> Maybe a
 single env p =
-    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 1000 }
+    p env { instantiationState = emptyInstantiationState, unificationState = emptyUnificationState, gas = 30 }
    |> Search.one
    |> Maybe.map (Tuple.first << Tuple.first)
--- a/src/Bergamot/Search.elm
+++ b/src/Bergamot/Search.elm
@@ -1,4 +1,4 @@
-module Bergamot.Search exposing (Search, map, apply, andThen, pure, fail, yield, interleave, one)
+module Bergamot.Search exposing (Search, map, apply, andThen, pure, lazy, fail, yield, interleave, one)

 type SearchStep a
    = Empty
@@ -31,6 +31,9 @@ andThen f sa () =
 pure : a -> Search a
 pure a () = Found a (\() -> Empty)

+lazy : (() -> Search a) -> Search a
+lazy f () = f () ()
+
 fail : Search a
 fail () = Empty

--- a/src/Bergamot/Syntax.elm
+++ b/src/Bergamot/Syntax.elm
@@ -1,5 +1,6 @@
 module Bergamot.Syntax exposing
-    ( Term(..), Metavariable(..), UnificationVar(..)
+    ( Term(..), toString, map, andThen, Metavariable(..), UnificationVar(..)
+    , unMetavariable, unUnificationVar
    , instantiate, instantiateList, InstantiationState, emptyInstantiationState, resetVars
    , unify, unifyList, UnificationState, emptyUnificationState
    , reify
@@ -23,10 +24,38 @@ unUnificationVar (MkUnificationVar s) = s

 type Term a
    = IntLit Int
+    | FloatLit Float
    | StringLit String
    | Call Name (List (Term a))
    | Var a

+toString : (a -> String) -> Term a -> String
+toString fn t =
+    case t of
+        IntLit i -> String.fromInt i
+        FloatLit f -> String.fromFloat f
+        StringLit s -> "\"" ++ s ++ "\"" -- TODO: insufficient, need to escape
+        Call n ts -> n ++ "(" ++ String.join ", " (List.map (toString fn) ts) ++ ")"
+        Var a -> fn a
+
+map : (a -> b) -> Term a -> Term b
+map f t =
+    case t of
+        IntLit i -> IntLit i
+        FloatLit ft -> FloatLit ft
+        StringLit s -> StringLit s
+        Call n ts -> Call n (List.map (map f) ts)
+        Var a -> Var (f a)
+
+andThen : (a -> Term b) -> Term a -> Term b
+andThen f t =
+    case t of
+        IntLit i -> IntLit i
+        FloatLit ft -> FloatLit ft
+        StringLit s -> StringLit s
+        Call n ts -> Call n (List.map (andThen f) ts)
+        Var a -> f a
+
 type alias InstantiationState =
    { counter : Int
    , vars : Dict String UnificationVar
@@ -62,6 +91,7 @@ instantiate : Term Metavariable -> InstantiationState -> (Term UnificationVar, I
 instantiate mt is =
    case mt of
        IntLit i -> (IntLit i, is)
+        FloatLit f -> (FloatLit f, is)
        StringLit s -> (StringLit s, is)
        Call n mts -> Tuple.mapFirst (Call n) (instantiateList mts is)
        Var mv -> Tuple.mapFirst Var (metavariable mv is)
@@ -93,12 +123,21 @@ merge v1 v2 us =
                in
                    case (ui1.term, ui2.term) of
                        (Just t1, Just t2) ->
-                            unify t1 t2 us
-                            |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
+                            if occurs ui1.equivalence us t2 || occurs ui2.equivalence us t1
+                            then Nothing
+                            else
+                                unify t1 t2 us
+                                |> Maybe.map (\(t, usp) -> reconcile newEq (Just t) usp)
                        (Just t1, Nothing) ->
-                            Just (reconcile newEq (Just t1) us)
+                            if occurs ui2.equivalence us t1
+                            then Nothing
+                            else
+                                Just (reconcile newEq (Just t1) us)
                        (Nothing, Just t2) ->
-                            Just (reconcile newEq (Just t2) us)
+                            if occurs ui1.equivalence us t2
+                            then Nothing
+                            else
+                                Just (reconcile newEq (Just t2) us)
                        (Nothing, Nothing) ->
                            Just (reconcile newEq Nothing us)
            (Just ui1, Nothing) -> Just (reconcile (Set.insert v2s ui1.equivalence) ui1.term us)
@@ -112,13 +151,35 @@ set v t us =
    in
        case Dict.get vs us of
            Just ui ->
-                case ui.term of
-                    Just tp ->
-                        unify t tp us
-                        |> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
-                    Nothing ->
-                        Just (t, reconcile ui.equivalence (Just t) us)
-            Nothing -> Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
+                if occurs ui.equivalence us t
+                then Nothing
+                else
+                    case ui.term of
+                        Just tp ->
+                            unify t tp us
+                            |> Maybe.map (\(tpp, usp) -> (tpp, reconcile ui.equivalence (Just tpp) usp))
+                        Nothing ->
+                            Just (t, reconcile ui.equivalence (Just t) us)
+            Nothing ->
+                if occurs (Set.singleton vs) us t
+                then Nothing
+                else
+                    Just (t, Dict.insert vs { equivalence = Set.singleton vs, term = Just t } us)
+
+occurs : Set String -> UnificationState -> Term UnificationVar -> Bool
+occurs vars us t =
+    case t of
+        IntLit _ -> False
+        FloatLit _ -> False
+        StringLit _ -> False
+        Call n ts -> List.any (occurs vars us) ts
+        Var (MkUnificationVar v) -> if Set.member v vars then True else
+            case Dict.get v us of
+                Just { term } ->
+                    case term of
+                        Just tp -> occurs vars us tp
+                        Nothing -> False
+                _ -> False

 unifyList : List (Term UnificationVar) -> List (Term UnificationVar) -> UnificationState -> Maybe (List (Term UnificationVar), UnificationState)
 unifyList l1 l2 us =
@@ -133,6 +194,7 @@ unify : Term UnificationVar -> Term UnificationVar -> UnificationState -> Maybe
 unify t1 t2 us =
    case (t1, t2) of
        (IntLit i1, IntLit i2) -> if i1 == i2 then Just (t1, us) else Nothing
+        (FloatLit f1, FloatLit f2) -> if f1 == f2 then Just (t1, us) else Nothing
        (StringLit s1, StringLit s2) -> if s1 == s2 then Just (t1, us) else Nothing
        (Call n1 ts1, Call n2 ts2) ->
            if n1 == n2
@@ -149,6 +211,7 @@ reify : Term UnificationVar -> UnificationState -> Term UnificationVar
 reify t us =
    case t of
        IntLit i -> IntLit i
+        FloatLit f -> FloatLit f
        StringLit s -> StringLit s
        Call n ts -> Call n (List.map (\tp -> reify tp us) ts)
        Var v ->
--- a/src/Bergamot/Utils.elm
+++ b/src/Bergamot/Utils.elm
@@ -0,0 +1,46 @@
+module Bergamot.Utils exposing (..)
+
+decodeStr : String -> String
+decodeStr str =
+    let
+        go l =
+            case l of
+                '\\' :: '"' :: rest -> '"' :: go rest
+                '\\' :: c :: rest -> c :: go rest
+                c :: rest -> c :: go rest
+                [] -> []
+        noQuotes = String.dropLeft 1 <| String.dropRight 1 <| str
+    in
+        String.fromList (go (String.toList str))
+
+encodeStr : String -> String
+encodeStr s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> '\\' :: '\\' :: go xs
+                '"' :: xs -> '\\' :: '"' :: go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        String.fromList (go (String.toList s))
+
+encodeLatex : String -> String
+encodeLatex s =
+    let
+        go l =
+            case l of
+                '\\' :: xs -> String.toList "\\textbackslash " ++ go xs
+                '{' :: xs -> '\\' :: '{' :: go xs
+                '}' :: xs -> '\\' :: '}' :: go xs
+                x :: xs -> x :: go xs
+                [] -> []
+    in
+        String.fromList (go (String.toList s))
+
+sequenceMaybes : List (Maybe a) -> Maybe (List a)
+sequenceMaybes l =
+    case l of
+        [] -> Just []
+        (Just x :: mxs) -> sequenceMaybes mxs |> Maybe.map (\xs -> x :: xs)
+        _ -> Nothing
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -1,75 +1,360 @@
-module Main exposing (main)
+port module Main exposing (main)

 import Browser
 import Html exposing (Html)
-import Html.Events exposing (onInput)
-import Html.Attributes exposing (type_, class, value)
+import Html.Events exposing (onInput, onClick)
+import Html.Attributes exposing (type_, class, classList, value)
+import Html.Lazy
 import Bergamot.Syntax exposing (..)
 import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
+import Bergamot.Utils exposing (..)
 import Json.Encode
+import Json.Decode exposing (string, field, list, oneOf, succeed, fail)
 import Maybe
 import Tuple
-import Debug
+
+type Tab
+    = Editor
+    | MetaEditor
+    | Rendered
+
+tabEq : Tab -> Tab -> Bool
+tabEq t1 t2 =
+    case (t1, t2) of
+        (Editor, Editor) -> True
+        (MetaEditor, MetaEditor) -> True
+        (Rendered, Rendered) -> True
+        _ -> False
+
+type EditMode
+    = Query
+    | Custom String
+
+type ResultMode
+    = Conclusion
+    | Tree
+
+type DesugaringState
+    = Requested
+    | Succeeded String
+    | Failed String
+
+resultModeEq : ResultMode -> ResultMode -> Bool
+resultModeEq rm1 rm2 =
+    case (rm1, rm2) of
+        (Conclusion, Conclusion) -> True
+        (Tree, Tree) -> True
+        _ -> False

 type alias Model =
    { program : String
-    , query : String
+      -- ^ The Bergamot rules to execute a search against
+    , renderProgram: String
+      -- ^ The Bergamot render rules to apply when generating LaTeX
+    , tab : Tab
+      -- ^ The current tab (editor, redner rule editor, rendered)
+    , input : String
+      -- ^ The string the user has in the input box
+    , desugaredQuery : DesugaringState
+      -- ^ The Bergamot query corresponding to input, if we're in custom mode.
+    , inputModes : List (String, EditMode)
+      -- ^ A List of input modes that can be used with the input box.
+    , inputMode : Int
+      -- ^ The index of the currently selected input mode.
+    , resultMode : ResultMode
+      -- ^ How the result should be displayed (judgement or proof tree)
+    }
+type alias Flags =
+    { renderRules : String
+    , rules : String
+    , input : String
+    , inputModes : Json.Decode.Value
    }
-type alias Flags = { rules: String, query: String }
 type Msg
    = SetProgram String
-    | SetQuery String
+    | SetRenderProgram String
+    | SetInput String
+    | SetTab Tab
+    | SetInputMode Int
+    | SetResultMode ResultMode
+    | SetDesugaredQuery { input: String, result: Json.Decode.Value }
+
+decodeRenderResult : Json.Decode.Value -> Result String String
+decodeRenderResult val =
+    let
+        succeedDecoder = field "query" string |> Json.Decode.map Ok
+        failDecoder = field "error" string |> Json.Decode.map Err
+        decoder = Json.Decode.oneOf [ succeedDecoder, failDecoder ]
+    in
+        case Json.Decode.decodeValue decoder val of
+            Ok v -> v
+            Err _ -> Err "Unable to convert input into query"
+
+decodeInputModes : Json.Decode.Value -> List (String, EditMode)
+decodeInputModes val =
+    let
+        exactString s1 v =
+            string
+            |> Json.Decode.andThen (\s2 ->
+                if s1 == s2
+                then succeed v
+                else Json.Decode.fail "did not match expected string")
+        editModeDecoder = oneOf
+            [ exactString "query" Query
+            , field "custom" string |> Json.Decode.map Custom
+            ]
+        decoder = Json.Decode.keyValuePairs editModeDecoder
+    in
+        case Json.Decode.decodeValue decoder val of
+            Ok l -> l
+            Err _ -> [("Query", Query)]
+
+-- Convert the user-entered string 'input' using custom query mode 'mode'
+port convertInput : { mode : String, input : String } -> Cmd msg
+
+-- Invoked when user code finishes converting 'input' into a Bergamot query
+port receiveConverted : ({ input : String, result : Json.Decode.Value } -> msg) -> Sub msg
+
+requestDesugaring : Int -> List (String, EditMode) -> String -> Cmd Msg
+requestDesugaring inputMode inputModes input =
+    case getEditMode inputMode inputModes of
+        Ok (Custom modeType) ->
+            convertInput { mode = modeType, input = input }
+        _ -> Cmd.none

 init : Flags -> (Model, Cmd Msg)
-init fs = ({ program = fs.rules, query = fs.query }, Cmd.none)
+init fs =
+    let
+        inputModes = decodeInputModes fs.inputModes
+        inputMode = 0
+    in
+        ( { program = fs.rules
+          , renderProgram = fs.renderRules
+          , input = fs.input
+          , desugaredQuery = Requested
+          , tab = Rendered
+          , inputModes = inputModes
+          , inputMode = 0
+          , resultMode = Conclusion
+          }
+        , requestDesugaring inputMode inputModes fs.input
+        )

 viewSection : String -> Html Msg -> Html Msg
 viewSection name content =
    Html.div [ class "bergamot-section" ] [ Html.em [ class "bergamot-section-heading" ] [ Html.text name ], content ]

-viewRule : Rule -> Html Msg
-viewRule = latex << ruleToLatex
+viewTab : Tab -> Html Msg -> Html Msg -> Html Msg -> Html Msg
+viewTab tab editor metaEditor rendered =
+    case tab of
+        Editor -> editor
+        MetaEditor -> metaEditor
+        Rendered -> rendered

-viewRules : String -> Html Msg
-viewRules progs = viewSection "Rendered Rules" <|
-    Html.div [ class "bergamot-rule-list" ] <|
-        case run program progs of
-            Just prog -> List.map viewRule prog.rules
-            Nothing -> []
+viewSelector : (Int -> a -> b -> Bool) -> (Int -> a -> Msg) -> b -> List (a, String) -> Html Msg
+viewSelector eq mkMsg mode modeNames =
+    Html.div [ class "bergamot-selector" ] <|
+        List.indexedMap (\idx (modep, name) ->
+            Html.button
+                [ classList [("active", eq idx modep mode)]
+                , onClick (mkMsg idx modep)
+                ] [ Html.text name ]) modeNames

-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
+viewTabSelector : Tab -> List (Tab, String) -> Html Msg
+viewTabSelector = viewSelector (\_ -> tabEq) (\_ -> SetTab)

-viewProofTree : String -> String -> Html Msg
-viewProofTree progs querys = viewSection "Proof Tree" <|
-    Html.div [ class "bergamot-proof-tree" ] <|
-      case tryProve progs querys of
-          Just tree -> [ latex (proofTreeToLatex tree) ]
-          Nothing -> []
+viewInputModeSelector : Int -> List (EditMode, String) -> Html Msg
+viewInputModeSelector = viewSelector (\i _ idx -> i == idx) (\idx _ -> SetInputMode idx)

+viewResultModeSelector : ResultMode -> List (ResultMode, String) -> Html Msg
+viewResultModeSelector = viewSelector (\_ -> resultModeEq) (\_ -> SetResultMode)
+
+viewRule : RuleEnv -> Rule -> Maybe (Html Msg)
+viewRule env r = renderRuleViaRules env r
+    |> Maybe.map latex
+
+viewRuleSection : RuleEnv -> Section -> Maybe (Html Msg)
+viewRuleSection env sec =
+    List.map (viewRule env) sec.rules
+    |> sequenceMaybes
+    |> Maybe.map (\rs ->
+        case sec.hidden of
+            True -> Html.div [ class "bergamot-rule-section" ] []
+            False ->
+                Html.div [ class "bergamot-rule-section" ]
+                [ Html.div [ class "bergamot-rule-list" ] rs
+                , Html.p [class "bergamot-rule-section-name"] [Html.text (sec.name)]
+                ])
+
+viewRules : String -> String -> Html Msg
+viewRules renderProgs progs =
+    Html.div [ class "bergamot-section-list" ] <|
+        case progAndRenderProg progs renderProgs of
+            Ok (prog, renderProg) -> List.filterMap (viewRuleSection renderProg) prog.sections
+            _ -> []
+
+type Error
+    = BadQuery
+    | NoConversionResults
+    | BadInputProg
+    | BadProg
+    | BadRenderProg
+    | FailedRender String
+    | InvalidInputMode
+    | Silent
+
+combineTwoResults : (a -> b -> Result Error c) -> Result Error a -> Result Error b -> Result Error c
+combineTwoResults f ra rb =
+    case ra of
+        Err _ -> Err Silent
+        Ok a ->
+            case rb of
+                Err _ -> Err Silent
+                Ok b -> f a b
+
+errorToString : Error -> String
+errorToString err =
+    case err of
+        BadQuery -> "Unable to parse input query"
+        NoConversionResults -> "Failed to convert object language term to proof goal"
+        BadInputProg -> "Unable to parse conversion rules from object language to proof goals"
+        BadProg -> "Unable to parse rules"
+        BadRenderProg -> "Unable to parse rendering rules"
+        FailedRender s -> s
+        InvalidInputMode -> "Invalid edit mode specified"
+        Silent -> ""
+
+viewError : Error -> Html Msg
+viewError e = Html.div [ class "bergamot-error" ] [ Html.text <| errorToString e ]
+
+viewIfError : Result Error a -> List (Html Msg)
+viewIfError r =
+    case r of
+        Err Silent -> []
+        Err e -> [ viewError e ]
+        _ -> []
+
+viewOrError : Result Error (Html Msg) -> Html Msg
+viewOrError r =
+    case r of
+        Err Silent -> Html.div [] []
+        Err e -> Html.div [] [ viewError e ] -- The div wrapper is needed because Elm has a bug?
+        Ok html -> html
+
+getEditMode : Int -> List (String, EditMode) -> Result Error EditMode
+getEditMode i l =
+    case l of
+        [] -> Err InvalidInputMode
+        ((_, editMode) :: xs) ->
+            if i == 0 then Ok editMode else getEditMode (i - 1) xs
+
+proofGoal : EditMode -> String -> DesugaringState -> Result Error (Term Metavariable)
+proofGoal editMode input desugaredQuery =
+    if input == ""
+    then Err Silent
+    else
+        case editMode of
+            Query ->
+                case run topLevelTerm input of
+                    Nothing -> Err BadQuery
+                    Just query -> Ok query
+            Custom _ ->
+                case desugaredQuery of
+                    Requested -> Err Silent
+                    Succeeded querys ->
+                        case run topLevelTerm querys of
+                            Nothing -> Err BadQuery
+                            Just query -> Ok query
+                    Failed s -> Err (FailedRender s)
+
+progAndRenderProg : String -> String -> Result Error (RuleEnv, RuleEnv)
+progAndRenderProg progs renderProgs =
+    case (run program progs, run program renderProgs) of
+        (Just prog, Just renderProg) -> Ok (prog, renderProg)
+        (Nothing, _) -> Err BadProg
+        (_, Nothing) -> Err BadRenderProg
+
+renderProofTree : ResultMode -> ProofTree -> RuleEnv -> Result Error (Html Msg)
+renderProofTree resultMode (MkProofTree node) renderProg =
+    let
+        maybeLatexString =
+            case resultMode of
+                Conclusion -> renderTermViaRules renderProg (quoteVariables node.conclusion)
+                Tree -> renderTreeViaRules renderProg (MkProofTree node)
+    in
+        List.filterMap (Maybe.map latex) [maybeLatexString]
+        |> Html.div [ class "bergamot-proof-tree" ]
+        |> Ok
+
+
+viewProofTree : ResultMode -> Term Metavariable -> (RuleEnv, RuleEnv) -> Result Error (Html Msg)
+viewProofTree resultMode query (prog, renderProg) =
+    case single prog (prove query |> Bergamot.Rules.andThen reifyProofTree) of
+        Just proofTree -> renderProofTree resultMode proofTree renderProg
+        Nothing -> Ok <| Html.div [ class "bergamot-no-proofs" ]
+            [ Html.text "No applicable rules to prove input" ]

 view : Model -> Html Msg
-view m = Html.div [ class "bergamot-root" ]
-    [ 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
-    ]
+view m =
+    let
+        mode = getEditMode m.inputMode m.inputModes
+        termOrErr = mode |> Result.andThen (\editMode -> proofGoal editMode m.input m.desugaredQuery)
+        progsOrErr = progAndRenderProg m.program m.renderProgram
+        proofTreeOrErr = combineTwoResults (viewProofTree m.resultMode) termOrErr progsOrErr
+    in
+        Html.div [ class "bergamot-root" ]
+        [ viewSection "Input" <| Html.div [] <|
+            [ viewInputModeSelector m.inputMode <|
+                List.map (\(a, b) -> (b, a)) m.inputModes
+            , Html.input [ type_ "text", onInput SetInput, value m.input ] []
+            ] ++
+            viewIfError termOrErr
+        , viewSection "Result" <| Html.div[]
+            [ viewResultModeSelector m.resultMode [(Conclusion, "Conclusion Only"), (Tree, "Full Proof Tree")]
+            , viewOrError proofTreeOrErr
+            ]
+        , viewSection "Rules" <| Html.div [] <|
+            [ viewTabSelector m.tab [(Rendered, "Rendered"), (Editor, "Editor"), (MetaEditor, "Presentation Rules")]
+            , viewTab m.tab
+                (Html.textarea [ onInput SetProgram, value m.program ] [ ])
+                (Html.textarea [ onInput SetRenderProgram, value m.renderProgram ] [ ])
+                (Html.Lazy.lazy2 viewRules m.renderProgram m.program)
+            ] ++
+            viewIfError progsOrErr
+        ]

 update : Msg -> Model -> (Model, Cmd Msg)
 update msg m =
    case msg of
        SetProgram prog -> ({ m | program = prog }, Cmd.none)
-        SetQuery query -> ({ m | query = query }, Cmd.none)
+        SetRenderProgram prog -> ({ m | renderProgram = prog }, Cmd.none)
+        SetInput input ->
+            ( { m | input = input, desugaredQuery = Requested }
+            , requestDesugaring m.inputMode m.inputModes input
+            )
+        SetTab tab -> ({ m | tab = tab }, Cmd.none)
+        SetInputMode mode ->
+            ( { m | inputMode = mode, desugaredQuery = Requested }
+            , requestDesugaring mode m.inputModes m.input
+            )
+        SetResultMode mode -> ({ m | resultMode = mode }, Cmd.none)
+        SetDesugaredQuery data ->
+            ({ m | desugaredQuery =
+                if m.input == data.input
+                then
+                    case decodeRenderResult data.result of
+                        Ok q -> Succeeded q
+                        Err e -> Failed e
+                else m.desugaredQuery
+             }
+            , Cmd.none
+            )

 subscriptions : Model -> Sub Msg
-subscriptions _ = Sub.none
+subscriptions _ = receiveConverted SetDesugaredQuery

 main =
    Browser.element
Author	SHA1	Message	Date
Danila Fedorin	ceca48840e	Use stable version of NixOS for nixpkgs Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-26 22:30:08 +00:00
Danila Fedorin	000d95ae5b	Update flake.lock Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-26 21:25:04 +00:00
Danila Fedorin	2af1692bf4	Remove symeq Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-11-03 17:13:14 -08:00
Danila Fedorin	0b4a1f2ebd	Implement hidden sections Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-11-03 17:13:05 -08:00
Danila Fedorin	c77bb6f900	Add some forward-only arithmetic operations and make rho render as LaTeX Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-15 16:33:07 -07:00
Danila Fedorin	e7d3e840b3	Allow input mode code to provide custom error messages Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-15 10:21:38 -07:00
Danila Fedorin	a17ea205c7	Clear 'Failed' flag when input changes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:56:42 -07:00
Danila Fedorin	2a0db676bc	Remove useless inputRules flag Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:54:13 -07:00
Danila Fedorin	a7b3efe56c	Tweak API to support syntax errors in custom parsing Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:29:32 -07:00
Danila Fedorin	ec0b05ab51	Make 'language term' just a custom mode Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 22:24:29 -07:00
Danila Fedorin	bfc21c2928	Add support for custom modes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:43:02 -07:00
Danila Fedorin	d1fb4bfdc1	Update index.html to work with new setup Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:06:57 -07:00
Danila Fedorin	b6569d8ca0	Allow for customizing the "input mode" toolbar Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-09-07 21:02:15 -07:00
Danila Fedorin	14b63fccc2	Revert "Reduce gas for proof search" This reverts commit `6a952f8a15`.	2024-04-20 14:10:18 -07:00
Danila Fedorin	6a952f8a15	Reduce gas for proof search Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-04-20 14:05:50 -07:00
Danila Fedorin	cd9a048832	Optimize the Elm JS.	2023-12-30 20:04:12 -08:00
Danila Fedorin	f35a8d17e8	Add a text for no proofs	2023-12-29 00:07:14 -08:00
Danila Fedorin	98562eca2d	Use the same 'literal' term for all object language literals Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-26 13:19:15 -08:00
Danila Fedorin	0b3469b49a	Add string and float literals to the object language Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-26 13:15:56 -08:00
Danila Fedorin	b828c73e43	Tweak builtin rules to handle floats and more Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-26 13:08:24 -08:00
Danila Fedorin	4c12fee4aa	Support parsing float literals in Bergamot Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-26 13:08:09 -08:00
Danila Fedorin	29a95d2659	Add float literals to Bergamot Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-26 13:07:52 -08:00
Danila Fedorin	97fcae9c2c	Tweak render rules to handle precedence Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 18:32:15 -08:00
Danila Fedorin	c192193c57	Add some more builtins to support rendering rules Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 18:24:55 -08:00
Danila Fedorin	287562619d	Use 'value' for textarea inputs Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 13:51:44 -08:00
Danila Fedorin	7d07b2dee9	Put lazy2 back Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 13:45:40 -08:00
Danila Fedorin	10d1edbc32	Add error reporting Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 13:42:20 -08:00
Danila Fedorin	aac1c7f961	Rename some parser functions in ObjectLanguage.elm Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-25 11:51:50 -08:00
Danila Fedorin	bc83f0ed53	Add bidirectional inference for `int(?x)` and `str(?x)`. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-22 21:59:41 -08:00
Danila Fedorin	12d823e944	Configure prommpts via a Bergamot program, too. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-22 15:58:52 -08:00
Danila Fedorin	9fd60b4013	Reorganize the UI somewhat and add conclusion-only view Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-22 15:22:46 -08:00
Danila Fedorin	aa7fd44a6d	Slightly tweak code for proving a term Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-22 14:39:52 -08:00
Danila Fedorin	da470f5caa	Add an occurss check to avoid infinite terms Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-22 14:39:35 -08:00
Danila Fedorin	abd6a848f8	Add support for editing the meta rules Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 16:57:46 -08:00
Danila Fedorin	535c714b47	Remove yields and switch to depth-based gas. This considerably speeds up forward inference, but we do get lost when trying to prove more difficult things, or doing backwards search. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 16:47:56 -08:00
Danila Fedorin	363e52ec5e	Switch entirely to using rules to render rules. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 14:45:04 -08:00
Danila Fedorin	84c79ddb50	Render sections in widget Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 14:06:37 -08:00
Danila Fedorin	678e51f146	Allow implicit sections to have more than one rule Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 14:06:10 -08:00
Danila Fedorin	401883c1da	Update the object language parser to use 'number' and 'string' Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 14:05:03 -08:00
Danila Fedorin	fd301806c6	Add sections to the language syntax Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-21 13:31:53 -08:00
Danila Fedorin	18d524a0d2	Avoid checking for out-of-gas on each 'andThen' Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-02 23:46:24 -08:00
Danila Fedorin	d6d610c038	Save the current rules I'm using for rendering LaTeX. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-02 00:27:41 -08:00
Danila Fedorin	11dd5ee9fd	Put render rules separately from regular rules This should let us hide them from the user and maybe speed up rendering Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-02 00:25:23 -08:00
Danila Fedorin	1d3f3fd3f8	Use 'lazy' to speed up re-rendering Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-02 00:07:01 -08:00
Danila Fedorin	f964a60412	Perform metavariable substitution from quoting Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-02 00:06:33 -08:00
Danila Fedorin	1fca9171b1	Unify conclusion before instantiating premises to save some time Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 23:40:29 -08:00
Danila Fedorin	12fa4dc1fd	WIP: Use bergamot to render inference rules. Not the proof trees yet, but it should be about the same.	2023-12-01 23:31:43 -08:00
Danila Fedorin	549527d0cc	Add a 'call' primitive Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 18:15:32 -08:00
Danila Fedorin	905b760dd7	Fix a few bugs with encoding / decoding strings Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 18:15:17 -08:00
Danila Fedorin	a1ae15d84c	Add a new builtin to identify symbols Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:56:27 -08:00
Danila Fedorin	012c1b0d0c	Extract common utility functions and convert symbols to strings Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:40:39 -08:00
Danila Fedorin	1e12dc8032	Ensure metavariables aren't re-used in rules and queries Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:35:22 -08:00
Danila Fedorin	f4619672a9	Implement more builtins Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:26:34 -08:00
Danila Fedorin	faa65ff77b	Don't encode '\n' for now Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:26:08 -08:00
Danila Fedorin	66fbfd1962	Add necessary escape characters for LaTeX and pretty printing Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:25:39 -08:00
Danila Fedorin	22f3937523	Fix a parser bug to parse '1' as IntLit Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 16:24:19 -08:00
Danila Fedorin	3232d80376	Add syntax sugar for lists Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 14:11:40 -08:00
Danila Fedorin	a8f07dd422	Tweak pretty printing of LaTeX Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 14:09:12 -08:00
Danila Fedorin	e659172320	Add a builtin rule for string concatenation Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 13:10:51 -08:00
Danila Fedorin	546265f2e6	Add string literals to the term language Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 12:55:11 -08:00
Danila Fedorin	45a04cc59c	Add a mode for entering the object language to parse Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-12-01 11:31:38 -08:00
Danila Fedorin	51c78af138	Add an initial parser for the Bergamot 'object language'	2023-11-30 22:44:20 -08:00
Danila Fedorin	d9f9522365	Add a tab to switch between editor and rendered view	2023-11-30 21:29:37 -08:00